mathlib-initiative/mathlib-tactics huggingface dataset:
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 : p a b + 1 < 0
⊢ ↑n ^ p a b * ∑ u ∈ Ico (r i n) n, g ↑u / ↑u ^ (p a b + 1) ≤
    ↑n ^ p a b * ∑ u ∈ Ico (r i n) n, c₂ * g ↑n / ↑u ^ (p a b + 1)

Tactic:
gcongr with u hu
        rw [Finset.mem_Ico] at hu
        have hu' : u ∈ Set.Icc (r i n) n := ⟨hu.1, by lia⟩
        refine hn₂ u ?_
        rw [Set.mem_Icc]
        refine ⟨?_, by norm_cast; lia⟩
        calc c₁ * n ≤ r i n := by exact hn₁ i
                  _ ≤ u := by exact_mod_cast hu'.1

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

Tactic:
rw [← Real.rpow_add_one (by positivity) (p a b)]; ring

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

Tactic:
gcongr with u hu
        rw [Finset.mem_Ico] at hu
        have hu' : u ∈ Set.Icc (r i n) n := ⟨hu.1, by lia⟩
        refine hn₂ u ?_
        rw [Set.mem_Icc]
        refine ⟨?_, by norm_cast; lia⟩
        calc c₁ * n ≤ r i n := by exact hn₁ i
                  _ ≤ u := by exact_mod_cast hu'.1

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

Goal state before:
pp: case hbc
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
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
hfg₃ : ‖g u‖ ≤ 1 / 2 * f u
⊢ c₁ * f x ≤ f u

Tactic:
exact (hf₁ u ⟨hu_lb, hu_ub⟩).1

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

Tactic:
rw [← Real.rpow_add_one (by positivity) (p a b)]; ring

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 * ∑ u ∈ Ico (r i n) n, g ↑u / ↑u ^ (p a b + 1) ≥
    ↑n ^ p a b * ∑ u ∈ Ico (r i n) n, c₂ * g ↑n / ↑u ^ (p a b + 1)

Tactic:
gcongr with u hu
        rw [Finset.mem_Ico] at hu
        have hu' : u ∈ Set.Icc (r i n) n := ⟨hu.1, by lia⟩
        refine hn₂ u ?_
        rw [Set.mem_Icc]
        refine ⟨?_, by norm_cast; lia⟩
        calc c₁ * n ≤ r i n := by exact hn₁ i
                  _ ≤ u := by exact_mod_cast hu'.1

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 * ↑n * (1 - c₃) * (c₂ * g ↑n / (c₁ ^ (p a b + 1) * ↑n ^ (p a b + 1))) =
    ↑n ^ (p a b + 1) / ↑n ^ (p a b + 1) * (1 - c₃) * c₂ * g ↑n / c₁ ^ (p a b + 1)

Tactic:
rw [← Real.rpow_add_one (by positivity) (p a b)]; ring

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

Goal state before:
pp: case hbc
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
⊢ c₁ * f x ≤ f u

Tactic:
exact (hf₁ u ⟨hu_lb, hu_ub⟩).1

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case mp
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
y : List α
hy : y ∈ S ∧ ¬y = []
⊢ y ∈ l ∧ y ≠ []

Tactic:
exact ⟨h y hy.1, hy.2⟩

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case succ
α : 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 α
⊢ x ∈ l ^ (n + 1) ↔ ∃ S, x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l

Tactic:
| succ n ihn =>

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
⊢ l∗ * m ≤ m

Tactic:
rw [kstar_eq_iSup_pow, iSup_mul]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
⊢ ⨆ i, l ^ i * m ≤ m
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
⊢ reverse 1 = 1

Tactic:
by
  simp [reverse, ← one_def]

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

Goal state before:
pp: a : Bool
x : ℕ
⊢ bit a x % 2 = 0 ↔ (!a) = true

Tactic:
by
  simp

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

Goal state before:
pp: a : Bool
x : ℕ
⊢ bit a x % 2 = 1 ↔ a = true

Tactic:
by
  simp

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

Goal state before:
pp: b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
hj : k + 1 < 0
⊢ False

Tactic:
simp at hj

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

Goal state before:
pp: 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' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ n.testBit j = m.testBit j

Tactic:
convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]

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
hab : a ^^^ b = c ^^^ v
⊢ b ^^^ c = a ^^^ v

Tactic:
rw [← Nat.xor_assoc, Nat.xor_xor_cancel_left]

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

Goal state before:
pp: b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (c₁ * log x) (c₂ * log x)

Tactic:
refine ⟨1 / 2, by norm_num, ?_⟩

Goal state after:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
⊢ ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (1 / 2 * log x) (c₂ * log x)
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
κ : ι → Sort u_2
f : (i : ι) → κ i → Set σ
x : List α
⊢ M.evalFrom (⋃ i, ⋃ j, f i j) x = ⋃ i, ⋃ j, M.evalFrom (f i j) x

Tactic:
by
  simp

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

Goal state before:
pp: case mpr
α : Type u_1
l : List (Option α)
a : α
w✝¹ w✝ : ℕ
h : l = replicate w✝¹ none ++ some a :: replicate w✝ none
⊢ filterMap id l = [a]

Tactic:
simp only [h, filterMap_append, filterMap_cons_some, filterMap_replicate_of_none, id_eq,
      nil_append, Option.some.injEq]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
left; tauto

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
κ : ι → Sort u_2
f : (i : ι) → κ i → Set σ
⊢ M.acceptsFrom (⋃ i, ⋃ j, f i j) = ⋃ i, ⋃ j, M.acceptsFrom (f i j)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate 0 none)
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
rw [List.replicate_zero] at h

Goal state after:
case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ []
⊢ s₂ ∈ M.εClosure {s₁}
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ (↑n).size + 1 = (↑n.bit0).size

Tactic:
cast_bit0,

Goal state after:
n : PosNum
⊢ (↑n).size + 1 = (↑n + ↑n).size
Module: Mathlib.Computability.Halting

Goal state before:
pp: C : Set (ℕ →. ℕ)
h : ComputablePred fun c ↦ c.eval ∈ C
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
⊢ g ∈ C

Tactic:
obtain ⟨_, h⟩ := h
  obtain ⟨c, e⟩ :=
    fixed_point₂
      (Partrec.cond (h.comp fst) ((Partrec.nat_iff.2 hg).comp snd).to₂
          ((Partrec.nat_iff.2 hf).comp snd).to₂).to₂
  simp only [Bool.cond_decide] at e
  by_cases H : eval c ∈ C <;> simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ ↑n.bit1 = 2 * ↑n + 1

Tactic:
rw [← bit1_of_bit1, bit0_of_bit0, cast_add, cast_bit0]; rfl

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

Goal state before:
pp: m n : PosNum
⊢ n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
rw [← cmp_swap]; cases cmp m n <;> decide

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

Goal state before:
pp: m n : Num
⊢ n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
rw [← cmp_swap]; cases cmp m n <;> decide

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
⊢ ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
intro x h

Goal state after:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m : PosNum
⊢ ↑(bif g true false then pos m else 0) = if g true false = true then ↑(pos m) else 0

Tactic:
cases g true false <;> rfl

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

Goal state before:
pp: f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
⊢ GrowsPolynomially f

Tactic:
by
  have : f = g + (f - g) := by ext; simp
  rw [this]
  exact add_isLittleO hg hf

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab : Reaches f₁ a₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
by
  rcases reflTransGen_iff_eq_or_transGen.1 ab with (rfl | ab)
  · exact ⟨_, aa, ReflTransGen.refl⟩
  · have ⟨b₂, bb, h⟩ := tr_reaches₁ H aa ab
    exact ⟨b₂, bb, h.to_reflTransGen⟩

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ (ListBlank.map (proj k) L).nth n = S.reverse[n]?

Tactic:
hL,

Goal state after:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ (ListBlank.mk (List.map some S).reverse).nth n = S.reverse[n]?
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
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h : ¬i = (S k).length
⊢ (ListBlank.map (proj k) L).nth i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
hL,

Goal state after:
case neg
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h : ¬i = (S k).length
⊢ (ListBlank.mk (List.map some (S k)).reverse).nth i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i
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
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
i : ℕ
h : ¬i = tl.length
⊢ (ListBlank.map (proj k) L).nth i = (List.map some tl).reverse.getI i

Tactic:
hL,

Goal state after:
case neg
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
i : ℕ
h : ¬i = tl.length
⊢ (ListBlank.mk (List.map some (S k)).reverse).nth i = (List.map some tl).reverse.getI i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case rfind
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
IHf : ∃ c, ∀ (v : List.Vector ℕ (n + 1)), c.eval ↑v = pure <$> ↑f v
⊢ ∃ c,
    ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> (fun v ↦ Nat.rfind fun n_1 ↦ Part.some (decide (f (n_1 ::ᵥ v) = 0))) v

Tactic:
obtain ⟨cf, hf⟩ := IHf; refine ⟨rfind cf, fun v => ?_⟩
    replace hf := fun a => hf (a ::ᵥ v)
    simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, PFun.coe_val,
      show ∀ x, pure x = [x] from fun _ => rfl] at hf ⊢
    refine Part.ext fun x => ?_
    simp only [rfind, Part.bind_eq_bind, Part.pure_eq_some, Part.bind_some,
      cons_eval, comp_eval, fix_eval, tail_eval, succ_eval, zero'_eval,
      List.headI_cons, pred_eval, Part.map_some, false_eq_decide_iff,
      Part.mem_bind_iff, Part.mem_map_iff, Nat.mem_rfind,
      List.tail_cons, true_eq_decide_iff, Part.mem_some_iff, Part.map_bind]
    constructor
    · rintro ⟨v', h1, rfl⟩
      suffices ∀ v₁ : List ℕ, v' ∈ PFun.fix
        (fun v => (cf.eval v).bind fun y => Part.some <|
          if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail)
            else Sum.inr (v.headI.succ :: v.tail)) v₁ →
        ∀ n, (v₁ = n :: v.val) → (∀ m < n, ¬f (m ::ᵥ v) = 0) →
          ∃ a : ℕ,
            (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
        by exact this _ h1 0 rfl (by rintro _ ⟨⟩)
      clear h1
      intro v₀ h1
      refine PFun.fixInduction h1 fun v₁ h2 IH => ?_
      clear h1
      rintro n rfl hm
      have := PFun.mem_fix_iff.1 h2
      simp only [hf, Part.bind_some] at this
      split_ifs at this with h
      · simp only [List.headI_cons, exists_false, or_false, Part.mem_some_iff,
          List.tail_cons, false_and, Sum.inl.injEq, reduceCtorEq] at this
        subst this
        exact ⟨_, ⟨h, @hm⟩, rfl⟩
      · refine IH (n.succ::v.val) (by simp_all) _ rfl fun m h' => ?_
        obtain h | rfl := Nat.lt_succ_iff_lt_or_eq.1 h'
        exacts [hm _ h, h]
    · rintro ⟨n, ⟨hn, hm⟩, rfl⟩
      refine ⟨n.succ::v.1, ?_, rfl⟩
      have : (n.succ::v.1 : List ℕ) ∈
        PFun.fix (fun v =>
          (cf.eval v).bind fun y =>
            Part.some <|
              if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail)
                else Sum.inr (v.headI.succ :: v.tail))
            (n::v.val) :=
        PFun.mem_fix_iff.2 (Or.inl (by simp [hf, hn]))
      generalize (n.succ :: v.1 : List ℕ) = w at this ⊢
      clear hn
      induction n with
      | zero => exact this
      | succ n IH =>
        refine IH (fun {m} h' => hm (Nat.lt_succ_of_lt h'))
          (PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, this⟩))
        simp only [hf, hm n.lt_succ_self, Part.bind_some, List.headI, if_false,
          Part.mem_some_iff, List.tail_cons]

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

Goal state before:
pp: case mp
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
y : Cfg
h : x ∈ eval step y
IH :
  ∀ (a' : Cfg),
    step y = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = 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₂)
⊢ ∀ (v : List ℕ) (c' : Cfg),
    y = 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₂)

Tactic:
rintro v (⟨v'⟩ | ⟨k', v'⟩) rfl hr <;> rw [Cfg.then] at h IH

Goal state after:
case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step ((fun k' ↦ stepRet k' v') (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((fun k' ↦ stepRet k' v') (Cont.fix f k)) = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = 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₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
⊢ ∃ 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₂)

case mp.ret
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v : List ℕ
k' : Cont
v' : List ℕ
h : x ∈ eval step ((fun k'_1 ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((fun k'_1 ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k)) = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = 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₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.ret k' v')
⊢ ∃ 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₂)