mathlib-initiative/mathlib-tactics huggingface dataset:
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|
⊢ GrowsPolynomially fun x ↦ f x * g x

Tactic:
by
    cases eventually_atTop_nonneg_or_nonpos hf with
    | inl hf' =>
      cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]
        rwa [iff_eventuallyEq hmain]
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonneg hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg
    | inr hf' =>
      cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain]
        exact this

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, 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
⊢ ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)) =
    ↑n ^ p a b * (↑n - ↑(r i n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1))

Tactic:
by
          congr; 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: α : 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
⊢ c₂ * g ↑n * ↑n ^ (p a b + 1) / (c₁ * ↑n) ^ (p a b + 1) =
    c₂ * g ↑n * ↑n ^ (p a b + 1) / (↑n ^ (p a b + 1) * c₁ ^ (p a b + 1))

Tactic:
by
          rw [mul_comm c₁, Real.mul_rpow (by positivity) (by positivity)]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_2.prec
cf cg : Code
pf : Nat.Partrec cf.eval
pg : Nat.Partrec cg.eval
⊢ Nat.Partrec (cf.prec cg).eval

Tactic:
| prec cf cg pf pg =>

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 : ℕ) in atTop,
    ∀ (i : α), min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n ≤ sumTransform (p a b) g (r i n) n

Tactic:
filter_upwards [hc₁, hc₂, hc₃, R.eventually_r_pos, R.eventually_r_lt_n, eventually_gt_atTop 0]
    with n hn₁ hn₂ hn₃ hrpos hr_lt_n hn_pos

Goal state after:
α : 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 : α), min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n ≤ sumTransform (p a b) g (r i n) n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
⊢ (∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y) →
    0 ≤ x → ∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (c₁ / 3 * (f x + g x)) (3 * c₂ * (f x + g x))

Tactic:
hf₂

Goal state after:
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
⊢ 0 ≤ x → ∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (c₁ / 3 * (f x + g x)) (3 * c₂ * (f x + g x))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 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‖
⊢ (∀ (y : ℝ), b * id x ≤ y → f y ≤ 0) →
    0 ≤ x → ∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (3 * c₁ * (f x + g x)) (c₂ / 3 * (f x + g x))

Tactic:
hf₂

Goal state after:
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
⊢ 0 ≤ x → ∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (3 * c₁ * (f x + g x)) (c₂ / 3 * (f x + g x))
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n x : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : m = 0
h₂ : (unpair n).2 = x
⊢ 0 + (unpair n).2 = x

Tactic:
by simp [h₂]

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 : p a b + 1 < 0
⊢ ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / (c₁ * ↑n) ^ (p a b + 1)) =
    ↑n ^ p a b * (↑n - ↑(r i n)) * (c₂ * g ↑n / (c₁ * ↑n) ^ (p a b + 1))

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

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case right
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
simpa [a0, add_comm, add_left_comm] using
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂

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

Goal state before:
pp: case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
⊢ GrowsPolynomially fun x ↦ (f x)⁻¹

Tactic:
refine fun b hb => ⟨1, by simp, 1, by simp, ?_⟩

Goal state after:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ (f x)⁻¹) u ∈ Set.Icc (1 * (fun x ↦ (f x)⁻¹) x) (1 * (fun x ↦ (f x)⁻¹) x)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ (f x)⁻¹) u ∈ Set.Icc (1 * (fun x ↦ (f x)⁻¹) x) (1 * (fun x ↦ (f x)⁻¹) x)

Tactic:
have hb_pos := hb.1

Goal state after:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ (f x)⁻¹) u ∈ Set.Icc (1 * (fun x ↦ (f x)⁻¹) x) (1 * (fun x ↦ (f x)⁻¹) x)
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 s (a :: S).flatten = s

Tactic:
Set.mem_singleton_iff

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 s (a :: S).flatten = s
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inr
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
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (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)

Tactic:
have hb_pos := hb.1

Goal state after:
case inr
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₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (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)
Module: Mathlib.Computability.DFA

Goal state before:
pp: case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : c' ∈ {c}
a' : List α
ha' : a' ∈ {a}
b' : List α
hb' : b' ∈ {b}∗
⊢ a' ++ b' ++ c' ∈ M.accepts

Tactic:
Set.mem_singleton_iff

Goal state after:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : c' = c
a' : List α
ha' : a' = a
b' : List α
hb' : b' ∈ {b}∗
⊢ a' ++ b' ++ c' ∈ M.accepts
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (bitwise f)
⊢ bitwise f n m = bitwise f m n

Tactic:
conv_lhs => rw [this]

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

Goal state before:
pp: case inr.inl
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
right; left; rw [hca]

Goal state after:
case inr.inl
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
⊢ b ^^^ v < b
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
have hb_pos := hb.1

Goal state after:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a

Tactic:
by
  simp [stepSet]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s : σ
a : α
⊢ M.stepSet {s} a = M.step s a

Tactic:
by
  simp [stepSet]

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:
rw [isPath_iff]
  simp [eq_comm]

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

Goal state before:
pp: x✝ : Num
⊢ 0 * ↑x✝ = 0

Tactic:
zero_mul

Goal state after:
x✝ : Num
⊢ 0 = 0
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h✝ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ (List.replicate n none).reduceOption = [] ∧ M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
List.reduceOption_replicate_none

Goal state after:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h✝ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ [] = [] ∧ M.IsPath s₁ s₂ (List.replicate n none)
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

pp: case cons
Γ : Type ?u.5
inst✝ : Inhabited Γ
l : ListBlank Γ
i : ℕ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝).tail (head✝ :: tail✝ ++ List.replicate i default).tail

Tactic:
· rcases i with - | i <;> [exact ⟨0, rfl⟩; exact ⟨i, rfl⟩]

Goal state after:
case cons
Γ : Type ?u.5
inst✝ : Inhabited Γ
l : ListBlank Γ
i : ℕ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝).tail (head✝ :: tail✝ ++ List.replicate i default).tail
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun a ↦ ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b ↦ true) (Part.assert (p a) fun x ↦ Part.some ()) ∨
        x ∈ Part.map (fun b ↦ false) (Part.assert ((fun a ↦ ¬p a) a) fun x ↦ Part.some ())
⊢ Computable fun a ↦ decide (p a)

Tactic:
refine Partrec.of_eq pk fun n => Part.eq_some_iff.2 ?_

Goal state after:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun a ↦ ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b ↦ true) (Part.assert (p a) fun x ↦ Part.some ()) ∨
        x ∈ Part.map (fun b ↦ false) (Part.assert ((fun a ↦ ¬p a) a) fun x ↦ Part.some ())
n : α
⊢ (fun a ↦ decide (p a)) n ∈ k n
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = false
⊢ TM0.step (tr M) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T } =
    TM0.step (tr M) { q := (some a✝, v), Tape := T }

Tactic:
by simp only [TM0.step, tr, trAux, e]; rfl

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = true
⊢ TM0.step (tr M) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T } =
    TM0.step (tr M) { q := (some a✝¹, v), Tape := T }

Tactic:
by simp only [TM0.step, tr, trAux, e]; rfl

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

Goal state before:
pp: case right.some.some.branch.true
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (bif true then trAux M a q₁ v else trAux M a q₂ v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
h : p a v = true
⊢ q₁ ∈ insert (TM1.Stmt.branch p q₁ q₂) (TM1.stmts₁ q₁ ∪ TM1.stmts₁ q₂)

Tactic:
exact Finset.mem_insert_of_mem (Finset.mem_union_left _ TM1.stmts₁_self)

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ↔
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
constructor <;> rintro ⟨t, u, h, hP, hQ⟩

Goal state after:
case neg.mp
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : x = t ++ u
hP : (P.deriv a).rmatch t = true
hQ : Q.rmatch u = true
⊢ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

case neg.mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : a :: x = t ++ u
hP : P.rmatch t = true
hQ : Q.rmatch u = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l)) ∧
    ∀ q' ∈ writes (Stmt.goto l), SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
simp only [writes, Finset.notMem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      refine supportsStmt_read _ fun a _ s ↦ ?_
      exact Finset.mem_biUnion.2 ⟨_, hs _ _, Finset.mem_insert_self _ _⟩

Goal state after: