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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun L b ↦ ∀ a ∈ L, R a b

Tactic:
classical
  have h (L) (b) : (List.filter (R · b) L).length = L.length ↔ ∀ a ∈ L, R a b := by simp
  apply PrimrecRel.of_eq ?_ h
  exact (Primrec.eq.comp (list_length.comp <| PrimrecRel.listFilter hf) (.comp list_length fst))

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
_h : 0 < n + 1
⊢ ack (m + 1) 0 < ack (m + 1) (n + 1)

Tactic:
by
    rw [ack_succ_zero, ack_succ_succ]
    exact ack_strictMono_right _ (one_lt_ack_succ_left m n)

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ (ack (m + 1) (n + 1) + 1) ^ 2 ≤ ack (m + 1 + 3) (n + 1)

Tactic:
rw [ack_succ_succ, ack_succ_succ]
    apply (ack_add_one_sq_lt_ack_add_three _ _).trans (ack_mono_right _ <| ack_mono_left _ _)
    lia

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
⊢ Partrec f.fix

Tactic:
have hF : Partrec₂ F :=
    Partrec.nat_rec snd (sumInr.comp fst).partrec
      (sumCasesOn_right (snd.comp snd) (snd.comp <| snd.comp fst).to₂ (hf.comp snd).to₂).to₂

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
hF : Partrec₂ F
⊢ Partrec f.fix
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ rf
⊢ let PR := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg);
  let CO := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg);
  let PC := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg);
  let RF := fun a cf hf ↦ rf a (cf, hf);
  let F := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a);
  Primrec fun a ↦ F a (c a)

Tactic:
intro _

Goal state after:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ rf
PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg)
⊢ let CO := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg);
  let PC := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg);
  let RF := fun a cf hf ↦ rf a (cf, hf);
  let F := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO a) (PC a) (RF a);
  Primrec fun a ↦ F a (c a)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n) ≤ ack (max a b + 9) (m + (n + 1))

Tactic:
apply (ack_strictMono_right _ IH).le.trans

Goal state after:
case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (ack (max a b + 9) (m + n)) ≤ ack (max a b + 9) (m + (n + 1))
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p x : ℝ
hx : 1 < x
hderiv : deriv (fun x ↦ 1 - ε x) x = x⁻¹ / log x ^ 2
⊢ deriv (fun x ↦ x ^ p) x * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2) =
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)

Tactic:
Real.deriv_rpow_const

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

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

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Goal state after:
p x : ℝ
hx : 0 < x
⊢ p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / log x ^ 2
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

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

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Goal state after:
p x : ℝ
hx : 0 < x
⊢ p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / log x ^ 2
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)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
⊢ (fun x ↦ x ^ p a b * x⁻¹) =ᶠ[atTop] fun x ↦ x ^ (p a b - 1)

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

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 : ℝ
hx : 0 < x
⊢ x ^ p a b * x⁻¹ = x ^ (p a b - 1)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : n ≠ 0
this : 0 < b i
⊢ (log ↑n - (log (b i) + log ↑n)) / ((log (b i) + log ↑n) * log ↑n) =
    (log ↑n - log (b i) - log ↑n) / ((log (b i) + log ↑n) * log ↑n)

Tactic:
sub_add_eq_sub_sub

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : n ≠ 0
this : 0 < b i
⊢ (log ↑n - log (b i) - log ↑n) / ((log (b i) + log ↑n) * log ↑n) =
    (log ↑n - log (b i) - log ↑n) / ((log (b i) + log ↑n) * log ↑n)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
⊢ let PR := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg);
  let CO := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg);
  let PC := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg);
  let RF := fun a cf hf ↦ rf a (cf, hf);
  let F := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a);
  Computable fun a ↦ F a (c a)

Tactic:
intro _

Goal state after:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg)
⊢ let CO := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg);
  let PC := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg);
  let RF := fun a cf hf ↦ rf a (cf, hf);
  let F := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO a) (PC a) (RF a);
  Computable fun a ↦ F a (c a)
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)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
⊢ (fun x ↦ x ^ p a b * x⁻¹) =ᶠ[atTop] fun x ↦ x ^ (p a b - 1)

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

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 : ℝ
hx : 0 < x
⊢ x ^ p a b * x⁻¹ = x ^ (p a b - 1)
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, 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
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
⊢ g x ≤ ‖g x‖

Tactic:
exact le_norm_self (g x)

Goal state after:
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
⊢ g x ≤ ‖g x‖

Tactic:
exact le_norm_self (g x)

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + ((unpair n).2 + 1)))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some (y + ((unpair n).2 + 1))
i : ℕ
im : i < y + 1
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + (unpair n).2)), ¬a = 0

Tactic:
rcases i with - | i

Goal state after:
case neg.zero
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + ((unpair n).2 + 1)))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some (y + ((unpair n).2 + 1))
im : 0 < y + 1
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (0 + (unpair n).2)), ¬a = 0

case neg.succ
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + ((unpair n).2 + 1)))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some (y + ((unpair n).2 + 1))
i : ℕ
im : i + 1 < y + 1
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2)), ¬a = 0
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 : shiftLeft' b m (n + 1) ≠ 0
⊢ (shiftLeft' b m (n + 1)).size = m.size + (n + 1)

Tactic:
simp only [shiftLeft', ne_eq] at h ⊢
    rw [size_bit h, Nat.add_succ]
    by_cases s0 : shiftLeft' b m n = 0
    case neg => rw [IH s0]
    rw [s0] at h ⊢
    cases b; · exact absurd rfl h
    have : shiftLeft' true m n + 1 = 1 := congr_arg (· + 1) s0
    rw [shiftLeft'_true_eq_mul_pow] at this
    obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
    simp only [Nat.zero_add, Nat.one_mul, Nat.pow_eq_one, succ_ne_self, false_or] at this
    rw [this, Nat.add_zero]

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

Goal state before:
pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ (b✝ :: n✝.bits).length = n✝.size.succ

pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ bit b✝ n✝ ≠ 0

Tactic:
· simp [ih]

Goal state after:
case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ bit b✝ n✝ ≠ 0
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case zero
h : 0 ≠ 0
⊢ ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false

Tactic:
exact False.elim (h rfl)

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

Goal state before:
pp: case neg
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i = 0
⊢ bit b n < bit b' m

Tactic:
obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
        simp only [testBit_bit_succ] at hn hm
        have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
        exact bit_lt_bit b b' this

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

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] → ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
intro h
    rw [reduceOption_eq_append_iff] at h
    obtain ⟨l₁, _, h, hl₁, hl₂⟩ := h
    rw [reduceOption_eq_singleton_iff] at hl₂
    obtain ⟨m, n, hl₂⟩ := hl₂
    use l₁ ++ replicate m none, replicate n none
    simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
      hl₂, and_self]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case base
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
h : a ∈ S
⊢ a ∈ S

pp: case step
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a s✝ : σ
a✝ : M.toεNFA.εClosure S s✝
h : a ∈ M.toεNFA.step s✝ none
⊢ a ∈ S

Tactic:
· exact h

Goal state after:
case step
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a s✝ : σ
a✝ : M.toεNFA.εClosure S s✝
h : a ∈ M.toεNFA.step s✝ none
⊢ a ∈ S
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ a ∈ S, x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ x✝ ∈ M.step a s

Tactic:
intro _

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ a✝ : σ
⊢ a✝ ∈ S → (x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a✝ (some s)) ↔ x✝ ∈ M.step a✝ s)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default

Tactic:
rw [List.append_assoc, ← List.replicate_add, Nat.sub_add_cancel]

Goal state after:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ j ≤ i
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case nil
Γ : Type ?u.5
inst✝ : Inhabited Γ
l : ListBlank Γ
i : ℕ
⊢ BlankExtends [].tail ([] ++ List.replicate i default).tail

Tactic:
rcases i with - | i

Goal state after:
case nil.zero
Γ : Type ?u.5
inst✝ : Inhabited Γ
l : ListBlank Γ
⊢ BlankExtends [].tail ([] ++ List.replicate 0 default).tail

case nil.succ
Γ : Type ?u.5
inst✝ : Inhabited Γ
l : ListBlank Γ
i : ℕ
⊢ BlankExtends [].tail ([] ++ List.replicate (i + 1) default).tail
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p : α → Prop
⊢ (∃ f, Computable f ∧ p = fun a ↦ f a = true) → ComputablePred p

Tactic:
rintro ⟨f, h, rfl⟩

Goal state after:
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
h : Computable f
⊢ ComputablePred fun a ↦ f a = true
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = if 0 = n + 1 then f (L.nth 0) else L.nth 0

pp: case succ.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
n✝ : ℕ
⊢ (modifyNth f (n + 1) L).nth (n✝ + 1) = if n✝ + 1 = n + 1 then f (L.nth (n✝ + 1)) else L.nth (n✝ + 1)

Tactic:
· rw [if_neg (Nat.succ_ne_zero _).symm]
      simp only [ListBlank.nth_zero, ListBlank.head_cons, ListBlank.modifyNth]

Goal state after:
case succ.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
n✝ : ℕ
⊢ (modifyNth f (n + 1) L).nth (n✝ + 1) = if n✝ + 1 = n + 1 then f (L.nth (n✝ + 1)) else L.nth (n✝ + 1)
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₁
hs : SupportsStmt S q
h : q₁ = move a✝ q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

Goal state after:
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₁
hs : SupportsStmt S q
h : q₁ = write a✝ q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

Goal state after:
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₁
hs : SupportsStmt S q
h : q₁ = load a✝ q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

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

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
⊢ ∀ {L' R' : ListBlank Bool} {l₁ l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
        Tape.mk' L' (ListBlank.append (enc a).toList R')

Tactic:
intro _

Goal state after:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ : ListBlank Bool
⊢ ∀ {R' : ListBlank Bool} {l₁ l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R')) =
        Tape.mk' L'✝ (ListBlank.append (enc a).toList R')
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

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

Tactic:
rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

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

Goal state before:
pp: case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
k✝ : K
a✝¹ : σ → Γ k✝
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ = push k✝ a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

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

Goal state before:
pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ = peek k✝ a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

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

Goal state before:
pp: case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ = pop k✝ a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

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

Goal state before:
pp: case some.branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q₁) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q₁ v (Tape.mk' L R)))
IH₂ :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q₂) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q₂ v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.branch p q₁ q₂)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.branch p q₁ q₂) v (Tape.mk' L R)))

Tactic:
simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, Tape.mk'_head]
      grind

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
⊢ ∀ {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), HasExplicitPullback coprod.inl f

Tactic:
intro _

Goal state after:
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ : CompHausLike P
⊢ ∀ {Y Z : CompHausLike P} (f : Z ⟶ X✝ ⨿ Y), HasExplicitPullback coprod.inl f