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

Goal state before:
pp: case inl
α : 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
⊢ sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g ↑n

Tactic:
| inl hp =>

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

Goal state before:
pp: case e_a.e_a
α : 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
⊢ ↑(#(Ico (r i n) n)) = ↑n - ↑(r i n)

Tactic:
rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]

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

Goal state before:
pp: case e_a.e_a
α : 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
⊢ ↑(#(Ico (r i n) n)) = ↑n - ↑(r i n)

Tactic:
rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]

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

Goal state before:
pp: case inl
α : 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
⊢ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n ≤ sumTransform (p a b) g (r i n) n

Tactic:
| inl hp =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.refine_1
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    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)))
          m =
        some 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))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
this : y ∈ evaln k.succ (cf.prec cg) (Nat.pair (unpair n).1 m)
⊢ 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)))
      m =
    some y

Tactic:
simp [evaln, Option.bind_eq_some_iff] at this

Goal state after:
case succ.refine_1
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    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)))
          m =
        some 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))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
this :
  Nat.pair (unpair n).1 m ≤ 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)))
        m =
      some y
⊢ 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)))
      m =
    some y
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case e_a.e_a
α : 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
⊢ ↑(#(Ico (r i n) n)) = ↑n - ↑(r i n)

Tactic:
rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
n : ℕ
ih : m * l ^ n ≤ m
⊢ m * l ^ (n + 1) ≤ m

Tactic:
pow_succ,

Goal state after:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
n : ℕ
ih : m * l ^ n ≤ m
⊢ m * (l ^ n * l) ≤ m
Module: Mathlib.Computability.Language

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ l ^ (n + 1) * m ≤ m

Tactic:
pow_succ,

Goal state after:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ l ^ n * l * m ≤ m
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t

Tactic:
obtain ⟨n, m, hneq, heq⟩ :=
    Fintype.exists_ne_map_eq_of_card_lt
      (fun n : Fin (Fintype.card σ + 1) => M.evalFrom s (x.take n)) (by simp)
  wlog hle : (n : ℕ) ≤ m generalizing n m
  · exact this m n hneq.symm heq.symm (le_of_not_ge hle)
  refine
    ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n,
                    x.drop m, ?_, ?_, ?_, by rfl, ?_⟩
  · rw [List.take_append_drop, List.take_append_drop]
  · simp only [List.length_drop, List.length_take]
    omega
  · intro h
    have hlen' := congr_arg List.length h
    simp only [List.length_drop, List.length, List.length_take] at hlen'
    omega
  have hq : M.evalFrom (M.evalFrom s ((x.take m).take n)) ((x.take m).drop n) =
      M.evalFrom s ((x.take m).take n) := by
    rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
  use hq
  rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc,
    List.take_append_drop, List.take_append_drop]

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
⊢ Tendsto (fun n ↦ 1 + ε ↑n) atTop (𝓝 1)

Tactic:
← Function.comp_def (fun n => 1 + ε n) Nat.cast

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto ((fun n ↦ 1 + ε n) ∘ Nat.cast) atTop (𝓝 1)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
n : ℕ
⊢ bitwise f n 0 = if f true false = true then n else 0

Tactic:
unfold bitwise
  simp only [ite_self, Nat.zero_div, ite_true, ite_eq_right_iff]
  rintro ⟨⟩
  split_ifs <;> rfl

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

Goal state before:
pp: f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ c₂⁻¹ * |f x|⁻¹ ≤ |f u|⁻¹

Tactic:
rw [← mul_inv]

Goal state after:
f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ (c₂ * |f x|)⁻¹ ≤ |f u|⁻¹
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u|⁻¹ ≤ c₁⁻¹ * |f x|⁻¹

Tactic:
rw [← mul_inv]

Goal state after:
f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u|⁻¹ ≤ (c₁ * |f x|)⁻¹
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case zero
n : ℕ
⊢ n.testBit 0 = n.bits.getI 0

Tactic:
simp only [testBit, shiftRight_zero, one_and_eq_mod_two, mod_two_of_bodd,
      bodd_eq_bits_head, List.getI_zero_eq_headI]

Goal state after:
case zero
n : ℕ
⊢ (n.bits.headI.toNat != 0) = n.bits.headI
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℕ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x ^ p

Tactic:
simp_rw [← rpow_natCast]

Goal state after:
f : ℝ → ℝ
p : ℕ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x ^ ↑p
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case nil
α : Type u_1
x : Option α
⊢ ([].concat x).reduceOption = [].reduceOption ++ x.toList

Tactic:
cases x <;> simp [Option.toList]

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

Goal state before:
pp: case cons
α : Type u_1
hd : Option α
tl : List (Option α)
hl : ∀ (x : Option α), (tl.concat x).reduceOption = tl.reduceOption ++ x.toList
x : Option α
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList

Tactic:
simp only [concat_eq_append, reduceOption_append] at hl
    cases hd <;> simp [hl, reduceOption_append]

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

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : α
⊢ (∃ i, l[i]? = some (some x)) ↔ ∃ i, l.reduceOption[i]? = some x

Tactic:
← mem_iff_getElem?,

Goal state after:
α : Type u_1
l : List (Option α)
x : α
⊢ some x ∈ l ↔ ∃ i, l.reduceOption[i]? = some x
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : α
⊢ some x ∈ l ↔ ∃ i, l.reduceOption[i]? = some x

Tactic:
← mem_iff_getElem?,

Goal state after:
α : Type u_1
l : List (Option α)
x : α
⊢ some x ∈ l ↔ x ∈ l.reduceOption
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ M.accepts
hlen : Fintype.card (Set σ) ≤ x.length
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Tactic:
rw [← toDFA_correct] at hx ⊢
  exact M.toDFA.pumping_lemma hx hlen

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ n, M.IsPath s₁ s₂ (List.replicate n none)) → s₂ ∈ M.εClosure {s₁}

Tactic:
by
    intro ⟨n, h⟩
    induction n generalizing s₂
    · rw [List.replicate_zero] at h
      apply IsPath.eq_of_nil at h
      solve_by_elim
    · simp_rw [List.replicate_add, isPath_append, List.replicate_one, isPath_singleton] at h
      obtain ⟨t, _, _⟩ := h
      solve_by_elim [εClosure.step]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil.mp
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ n, M.IsPath s₁ s₂ (List.replicate n none)) → ∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'

Tactic:
intro ⟨n, _⟩
      use List.replicate n none
      rw [List.reduceOption_replicate_none]
      trivial

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

Goal state before:
pp: n : PosNum
this : (↑n.pred').succ = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = (↑n + ↑n).pred

Tactic:
rw [← to_nat_inj.1 h]; rfl

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

Goal state before:
pp: b : Bool
n : PosNum
⊢ ↑(bit b n) = Nat.bit b ↑n

Tactic:
cases b <;> simp [bit, two_mul]

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range L.leftQuotient).Finite

Tactic:
← hM,

Goal state after:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range M.accepts.leftQuotient).Finite
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ List.flatMap f (l ++ List.replicate i default) = List.flatMap f l ++ List.replicate (i * n) default

Tactic:
rw [List.flatMap_append, mul_comm]

Goal state after:
Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ List.flatMap f l ++ List.flatMap f (List.replicate i default) = List.flatMap f l ++ List.replicate (n * i) default
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
⊢ stepAux (move n d q) v T = stepAux q v ((Tape.move d)^[n] T)

Tactic:
by
  suffices ∀ i, stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T) from this n
  intro i
  induction i generalizing T with
  | zero => rfl
  | succ i IH =>
    rw [iterate_succ', iterate_succ]
    simp only [stepAux, Function.comp_apply]
    rw [IH]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
R S : RegularExpression α
⊢ (map f (R * S)).matches' = (Language.map f) (R * S).matches'

Tactic:
simp [matches'_map]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
R : RegularExpression α
⊢ (map f R.star).matches' = (Language.map f) R.star.matches'

Tactic:
simp [matches'_map]

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

Goal state before:
pp: case comp
k' : Cont
c c' : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'

Tactic:
← ih',

Goal state after:
case comp
k' : Cont
c c' : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c' (Cont.comp c (k.then k')) v = stepNormal c' ((Cont.comp c k).then k') v
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h✝ : v₁.headI = 0
hv₂ : v₂ ∈ pure v₁.tail
⊢ Sum.inl v₂ ∈ Part.some (Sum.inl v₁.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inl v₁.tail) ∧
        v₂ ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) a'

Tactic:
rw [Part.mem_some_iff.1 hv₂]
        exact Or.inl (Part.mem_some _)

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

Goal state before:
pp: X : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
Z U : Set X
hZ : IsClosed[inst✝³] Z
hU : IsOpen[inst✝³] U
hZU : Z ⊆ U
V : ↑Z → Set X
hV : ∀ (z : ↑Z), IsClopen (V z) ∧ ↑z ∈ V z ∧ V z ⊆ U
⊢ ∃ C, IsClopen C ∧ Z ⊆ C ∧ C ⊆ U

Tactic:
have V_cover : Z ⊆ ⋃ z, V z := fun z hz ↦ mem_iUnion.mpr ⟨⟨z, hz⟩, (hV ⟨z, hz⟩).2.1⟩

Goal state after:
X : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
Z U : Set X
hZ : IsClosed[inst✝³] Z
hU : IsOpen[inst✝³] U
hZU : Z ⊆ U
V : ↑Z → Set X
hV : ∀ (z : ↑Z), IsClopen (V z) ∧ ↑z ∈ V z ∧ V z ⊆ U
V_cover : Z ⊆ ⋃ z, V z
⊢ ∃ C, IsClopen C ∧ Z ⊆ C ∧ C ⊆ U
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: 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)
⊢ { l := some default, var := default,
      Tape :=
        Tape.mk₁
          ((true, (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).headI.2) ::
            (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).tail) } =
    { l := Option.map normal (some default), var := default,
      Tape := Tape.mk' ∅ (addBottom (ListBlank.mk (List.map (fun a ↦ update default k (some a)) L.reverse))) }

Tactic:
congr <;> cases L.reverse

Goal state after:
case e_Tape.e_head.e_snd.nil
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)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) []).headI.2 =
    (ListBlank.mk (List.map (fun a ↦ update default k (some a)) [])).head

case e_Tape.e_head.e_snd.cons
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)
head✝ : Γ k
tail✝ : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) (head✝ :: tail✝)).headI.2 =
    (ListBlank.mk (List.map (fun a ↦ update default k (some a)) (head✝ :: tail✝))).head

case e_Tape.e_tail.nil
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)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) []).tail =
    List.map { f := Prod.mk false, map_pt' := ⋯ }.f (List.map (fun a ↦ update default k (some a)) []).tail

case e_Tape.e_tail.cons
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)
head✝ : Γ k
tail✝ : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) (head✝ :: tail✝)).tail =
    List.map { f := Prod.mk false, map_pt' := ⋯ }.f (List.map (fun a ↦ update default k (some a)) (head✝ :: tail✝)).tail