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

Goal state before:
pp: case zero
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_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
z : ℝ
x✝ : x ≤ z
hz : z ∈ Set.Icc (2⁻¹ * x₀) x₀
⊢ z ∈ Set.Icc (1 / 2 * x₀) x₀

Tactic:
simp only [one_div, hz]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
⊢ ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n

Tactic:
have h_max_bi_lt_one : 0 < 1 - b (max_bi b) := by
    have : b (max_bi b) < 1 := R.b_lt_one _
    linarith

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
⊢ ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
Module: Mathlib.Computability.AkraBazzi.SumTransform

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

Tactic:
rw [R.h_rec n hn]

Goal state after:
case ind.inr
α : 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
hn : R.n₀ ≤ n
⊢ 0 < ∑ i, a i * T (r i n) + g ↑n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: x : ℝ
⊢ deriv ε x = -x⁻¹ / log x ^ 2

Tactic:
deriv_smoothingFn

Goal state after:
x : ℝ
⊢ -x⁻¹ / log x ^ 2 = -x⁻¹ / log x ^ 2
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inr
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)
heq : c₁ = c₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
| inr hneg =>

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

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
x : ℝ
hx₁ : f x ≤ 0
hx₂ : 0 ≤ g x
⊢ f x * g x = - -f x * |g x|

Tactic:
abs_of_nonneg hx₂,

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
x : ℝ
hx₁ : f x ≤ 0
hx₂ : 0 ≤ g x
⊢ f x * g x = - -f x * g x
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_1
f : ℕ →. ℕ
h : Nat.Partrec f
⊢ ∃ c, c.eval = f

Tactic:
induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
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
⊢ c₂ * (1 - c₃) * g ↑n ≥ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n

Tactic:
gcongr; exact min_le_left _ _

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

Goal state before:
pp: case bc.a
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
⊢ ‖g x‖ ≤ -(1 / 2 * f x)

Tactic:
← neg_mul,

Goal state after:
case bc.a
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
⊢ ‖g x‖ ≤ -(1 / 2) * f x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case h₂
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
⊢ ‖g u‖ ≤ -(1 / 2 * f u)

Tactic:
← neg_mul,

Goal state after:
case h₂
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
⊢ ‖g u‖ ≤ -(1 / 2) * f u
Module: Mathlib.Computability.Language

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

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

Tactic:
· rintro ⟨a, ha, b, ⟨S, rfl, rfl, hS⟩, rfl⟩
      exact ⟨a :: S, rfl, rfl, forall_mem_cons.2 ⟨ha, hS⟩⟩

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

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

Tactic:
cases hn

Goal state after:
Module: Mathlib.Computability.Language

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

Tactic:
cases hn

Goal state after:
case succ.mpr.cons.refl
α : Type u_1
l : Language α
a : List α
S : List (List α)
hS : ∀ y ∈ a :: S, y ∈ l
ihn : ∀ {x : List α}, x ∈ l ^ S.length ↔ ∃ S_1, x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l
⊢ ∃ a_1 ∈ l, ∃ b, (∃ S_1, b = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l) ∧ a_1 ++ b = (a :: S).flatten
Module: Mathlib.Computability.DFA

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

Tactic:
rhs
    rw [Set.mem_preimage, mem_accepts]

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

Goal state before:
pp: case bit
b : Bool
n : ℕ
h : n = 0 → b = true
IH : n < 2 ^ n.size
⊢ bit b n < 2 ^ (bit b n).size

Tactic:
rw [← Nat.bit_ne_zero_iff] at h

Goal state after:
case bit
b : Bool
n : ℕ
h : bit b n ≠ 0
IH : n < 2 ^ n.size
⊢ bit b n < 2 ^ (bit b n).size
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: n : ℕ
⊢ n < 2 ^ n.size

Tactic:
by
  induction n using binaryRec' with
  | zero => simp
  | bit b n h IH =>
    rw [← Nat.bit_ne_zero_iff] at h
    rwa [size_bit h, bit_lt_two_pow_succ_iff]

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

Goal state before:
pp: n m k : ℕ
⊢ n &&& m &&& k = n &&& (m &&& k)

Tactic:
by bitwise_assoc_tac

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

Goal state before:
pp: n m k : ℕ
⊢ n ||| m ||| k = n ||| (m ||| k)

Tactic:
by bitwise_assoc_tac

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

Goal state before:
pp: a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
⊢ a ^^^ b = v ^^^ c

Tactic:
Nat.xor_xor_cancel_right

Goal state after:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
⊢ a ^^^ b = a ^^^ b
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ n % 2 = 0

Tactic:
rw [← @mod_mod_of_dvd _ 4 _ <| by simp, ← Fin.val_ofNat 4, h]

Goal state after:
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ ↑0 % 2 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0

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

Tactic:
· rw [this]

Goal state after:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ a.bit1 = b.bit1

pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a + 1

Tactic:
· rw [this]

Goal state after:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b c : Num
⊢ ↑a ≤ ↑b → ↑b ≤ ↑c → ↑a ≤ ↑c

Tactic:
apply le_trans

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

Goal state before:
pp: a b c : Num
⊢ 0 < ↑a → ↑b < ↑c → ↑a * ↑b < ↑a * ↑c

Tactic:
apply flip mul_lt_mul_of_pos_left

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

Goal state before:
pp: α : Type u_1
a b c : PosNum
⊢ ↑a ≤ ↑b → ↑b ≤ ↑c → ↑a ≤ ↑c

Tactic:
apply le_trans

Goal state after:
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✝
⊢ Partrec fun v ↦ Nat.rfind fun n ↦ Part.some (decide (f✝ (n ::ᵥ v) = 0))

Tactic:
have := hf.comp (vector_cons.comp snd fst)

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)
⊢ Partrec fun v ↦ Nat.rfind fun n ↦ Part.some (decide (f✝ (n ::ᵥ v) = 0))
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ Tape Γ

Tactic:
by constructor <;> apply default

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
⊢ Nat.RecursiveIn O f

Tactic:
induction pF with

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
c' : Cfg Γ Λ σ
h₁ : c' ∈ step M { l := some l₁, var := v, stk := T }
h₂ : { l := some l₁, var := v, stk := T }.l ∈ Finset.insertNone S
⊢ c'.l ∈ Finset.insertNone S

Tactic:
by
    replace h₂ := ss.2 _ (Finset.some_mem_insertNone.1 h₂)
    simp only [step, Option.mem_def, Option.some.injEq] at h₁; subst c'
    revert h₂; induction M l₁ generalizing v T with intro hs
    | branch p q₁' q₂' IH₁ IH₂ =>
      unfold stepAux; cases p v
      · exact IH₂ _ _ hs.2
      · exact IH₁ _ _ hs.1
    | goto => exact Finset.some_mem_insertNone.2 (hs _)
    | halt => apply Multiset.mem_cons_self
    | load _ _ IH | _ _ _ _ IH => exact IH _ _ hs

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

Goal state before:
pp: case pop.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (hd :: tl).tail k_1)).reverse) ∧
      (bif ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L))).head.1 then
          TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.1,
                update
                  (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k
                  none)
              (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (f v (hd :: tl).head?)
          ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom L')))

Tactic:
refine
        ⟨_, fun k' ↦ ?_, by
          erw [List.length_cons, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_succ_fst,
            cond_false, iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head,
            Tape.mk'_nth_nat, Tape.write_move_right_n fun a : Γ' K Γ ↦ (a.1, update a.2 k none),
            addBottom_modifyNth fun a ↦ update a k none, addBottom_nth_snd,
            stk_nth_val _ (hL k), e,
            show (List.cons hd tl).reverse[tl.length]? = some hd by
              rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length],
            List.head?, List.tail]⟩

Goal state after:
case pop.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
⊢ ListBlank.map (proj k') (ListBlank.modifyNth (fun a ↦ update a k none) tl.length L) =
    ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: c : Code
k k' : Cont
v : List ℕ
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'

Tactic:
by
  induction c generalizing k v with simp only [stepNormal, *]
  | cons c c' ih _ => rw [← ih, Cont.then]
  | comp c c' _ ih' => rw [← ih', Cont.then]
  | case => cases v.headI <;> simp only [Nat.rec_zero]
  | fix c ih => rw [← ih, Cont.then]
  | _ => simp only [Cfg.then]

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

Goal state before:
pp: case some
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
⊢ match TM2.step M { l := some l, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

Tactic:
rsuffices ⟨b, c, r⟩ : ∃ b, _ ∧ Reaches (TM1.step (tr M)) _ _

Goal state after:
case some
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
b : ?m.88
c : ?m.103 b
r : Reaches (TM1.step (tr M)) (?m.104 b) (?m.105 b)
⊢ match TM2.step M { l := some l, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
⊢ ∃ b, ?m.103 b ∧ Reaches (TM1.step (tr M)) (?m.104 b) (?m.105 b)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: ⊢ trNat 0 = []

Tactic:
trNat,

Goal state after:
⊢ trNum ↑0 = []
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
h : ¬k' = k
⊢ (Option.map (fun a ↦ update default k (some a) k') L.reverse[i]?).getD default =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i

Tactic:
simp only [Function.update_of_ne h]
      rw [ListBlank.nth_mk, List.getI_eq_getElem?_getD, List.map, List.reverse_nil]
      cases L.reverse[i]? <;> rfl

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case of_equiv
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
⊢ ∃ C,
    (∀ (i : β✝), IsClopen (C i)) ∧
      (∀ (i : β✝), Z i ⊆ C i) ∧ (∀ (i : β✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C

Tactic:
obtain ⟨C, h1, h2, h3, h4, h5⟩ := IH (Z := Z ∘ e) (D := D ∘ e)
      (fun i ↦ Z_closed (e i)) (fun i ↦ D_clopen (e i))
      (fun i ↦ Z_subset_D (e i)) (by simpa [← e.injective.injOn.pairwiseDisjoint_image])
    refine ⟨C ∘ e.symm, fun i ↦ h1 (e.symm i), fun i ↦ by simpa using h2 (e.symm i),
      fun i ↦ by simpa using h3 (e.symm i), ?_,
      by simpa [← e.symm.injective.injOn.pairwiseDisjoint_image]⟩
    simp only [Function.comp_apply, iUnion_subset_iff] at h4
    simpa [e.symm.surjective.iUnion_comp C] using fun i ↦ h4 (e.symm i)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
i j : J
f : i ⟶ j
V : Set ↑((F ⋙ toTopCat).obj j)
hV : IsClopen V
⊢ ⇑(ConcreteCategory.hom ((F ⋙ toTopCat).map f)) ⁻¹' V ∈ {W | IsClopen W}

Tactic:
refine ⟨hV.1.preimage ?_, hV.2.preimage ?_⟩

Goal state after:
case refine_2.refine_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
i j : J
f : i ⟶ j
V : Set ↑((F ⋙ toTopCat).obj j)
hV : IsClopen V
⊢ Continuous ⇑(ConcreteCategory.hom ((F ⋙ toTopCat).map f))

case refine_2.refine_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
i j : J
f : i ⟶ j
V : Set ↑((F ⋙ toTopCat).obj j)
hV : IsClopen V
⊢ Continuous ⇑(ConcreteCategory.hom ((F ⋙ toTopCat).map f))