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

Goal state before:
pp: case ha
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁⁻¹
h_ind : ∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
i : α
a✝ : i ∈ univ
j : ℕ
x✝ : j ∈ range (r i n)
⊢ 0 ≤ g ↑j ∧ 0 ≤ ↑j ^ (p a b + 1) ∨ g ↑j ≤ 0 ∧ ↑j ^ (p a b + 1) ≤ 0

Tactic:
exact Or.inl ⟨R.g_nonneg j (by positivity), by positivity⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n)
      n =
    some x
h : x ∈ Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n
⊢ x ∈ Nat.pair <$> evaln (k₂ + 1) cf n <*> evaln (k₂ + 1) cg n

Tactic:
simp only [Seq.seq, Option.map_eq_map, Option.mem_def, Option.bind_eq_some_iff,
          Option.map_eq_some_iff, exists_exists_and_eq_and] at h ⊢

Goal state after:
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n)
      n =
    some x
h : ∃ a, evaln (k + 1) cf n = some a ∧ ∃ a_1, evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ a, evaln (k₂ + 1) cf n = some a ∧ ∃ a_1, evaln (k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case ha
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
i : α
a✝ : i ∈ univ
j : ℕ
x✝ : j ∈ range (r i n)
⊢ 0 ≤ g ↑j ∧ 0 ≤ ↑j ^ (p a b + 1) ∨ g ↑j ≤ 0 ∧ ↑j ^ (p a b + 1) ≤ 0

Tactic:
exact Or.inl ⟨R.g_nonneg j (by positivity), by positivity⟩

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 α
n : ℕ
⊢ (if n + 1 = 0 then 0 else 1) = (if n = 0 then 0 else 1) + 1

Tactic:
cases n

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
⊢ (if 0 + 1 = 0 then 0 else 1) = (if 0 = 0 then 0 else 1) + 1

case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n✝ : ℕ
⊢ (if n✝ + 1 + 1 = 0 then 0 else 1) = (if n✝ + 1 = 0 then 0 else 1) + 1
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
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ ∑ i, a i * (↑(r i n) ^ p a b * (1 + ε ↑(r i n)) * (1 + ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1))) + C * g ↑n ≥
    ∑ i, a i * (b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) * (1 + ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1))) + C * g ↑n

Tactic:
by
      gcongr (∑ i, a i * (?_ *
          ((1 + (∑ u ∈ range (r i n), g u / u ^ ((p a b) + 1)))))) + C * g n with i
      · positivity [R.a_pos i]
      · refine add_nonneg zero_le_one <| Finset.sum_nonneg fun j _ => ?_
        rw [div_nonneg_iff]
        exact Or.inl ⟨R.g_nonneg j (by positivity), by positivity⟩
      · exact bound2 i

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
r : ContextFreeRule T N
p q : List (Symbol T N)
⊢ r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)

Tactic:
induction p with
  | nil => exact Rewrites.head q
  | cons d l ih => exact Rewrites.cons d ih

Goal state after:
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
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)
⊢ ∃ 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:
refine ⟨c₂⁻¹, by change 0 < c₂⁻¹; positivity, ?_⟩

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₁ : ℝ
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)
⊢ ∃ c₂_1 > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|⁻¹) u ∈ Set.Icc (c₂⁻¹ * (fun x ↦ |f x|⁻¹) x) (c₂_1 * (fun x ↦ |f x|⁻¹) x)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case bit
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : x = 0 → xb = true
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
        (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x y
y : ℕ
⊢ bitwise f (bit xb x) y =
    binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
      (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) (bit xb x) y

Tactic:
rw [← bit_ne_zero_iff] at hxb
    simp_rw [binaryRec_of_ne_zero _ _ hxb, bodd_bit, div2_bit, eq_rec_constant]
    induction y using binaryRec' with
    | zero => simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]
    | bit yb y hyb =>
      rw [← bit_ne_zero_iff] at hyb
      simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, div2_bit,
        bit_div_two, eq_rec_constant, ih]

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

Goal state before:
pp: n : PosNum
⊢ 1 + n = n.succ

Tactic:
cases n

Goal state after:
case one
⊢ 1 + one = one.succ

case bit1
a✝ : PosNum
⊢ 1 + a✝.bit1 = a✝.bit1.succ

case bit0
a✝ : PosNum
⊢ 1 + a✝.bit0 = a✝.bit0.succ
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ n + 1 = n.succ

Tactic:
cases n

Goal state after:
case one
⊢ one + 1 = one.succ

case bit1
a✝ : PosNum
⊢ a✝.bit1 + 1 = a✝.bit1.succ

case bit0
a✝ : PosNum
⊢ a✝.bit0 + 1 = a✝.bit0.succ
Module: Mathlib.Computability.Encoding

Goal state before:
pp: α : Type u_1
Γ : Type u_2
e : Encoding α Γ
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ some x✝¹ = some x✝

Tactic:
← e.decode_encode,

Goal state after:
α : Type u_1
Γ : Type u_2
e : Encoding α Γ
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ e.decode (e.encode x✝¹) = some x✝
Module: Mathlib.Computability.Encoding

Goal state before:
pp: α : Type u_1
Γ : Type u_2
e : Encoding α Γ
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ e.decode (e.encode x✝¹) = some x✝

Tactic:
← e.decode_encode,

Goal state after:
α : Type u_1
Γ : Type u_2
e : Encoding α Γ
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ e.decode (e.encode x✝¹) = e.decode (e.encode x✝)
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ filterMap id (replicate n none) = []

Tactic:
filterMap_replicate_of_none (id_def _)

Goal state after:
α : Type u_1
n : ℕ
⊢ [] = []
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp
α : Type u
σ : Type v
M : DFA α σ
x : List α
S : σ
hS₁ : S ∈ M.toNFA.accept
hS₂ : S ∈ {M.evalFrom M.start x}
⊢ x ∈ M.accepts

Tactic:
Set.mem_singleton_iff.mp hS₂

Goal state after:
case mp
α : Type u
σ : Type v
M : DFA α σ
x : List α
S : σ
hS₁ : M.evalFrom M.start x ∈ M.toNFA.accept
hS₂ : S ∈ {M.evalFrom M.start x}
⊢ x ∈ M.accepts
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : Num
⊢ n + 0 = n

Tactic:
cases n

Goal state after:
case zero
⊢ zero + 0 = zero

case pos
a✝ : PosNum
⊢ pos a✝ + 0 = pos a✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : Num
⊢ 0 + n = n

Tactic:
cases n

Goal state after:
case zero
⊢ 0 + zero = zero

case pos
a✝ : PosNum
⊢ 0 + pos a✝ = pos a✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ 0 < n.natSize

Tactic:
cases n

Goal state after:
case one
⊢ 0 < one.natSize

case bit1
a✝ : PosNum
⊢ 0 < a✝.bit1.natSize

case bit0
a✝ : PosNum
⊢ 0 < a✝.bit0.natSize
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
(choice (PosNum.transfer_rw "transfer_rw") (Num.transfer_rw "transfer_rw"))

Goal state after:
α : Type u_1
a b c : PosNum
⊢ ↑a ≤ ↑b → ↑b ≤ ↑c → ↑a ≤ ↑c
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
a b : PosNum
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
(choice (PosNum.transfer_rw "transfer_rw") (Num.transfer_rw "transfer_rw"))

Goal state after:
α : Type u_1
a b : PosNum
⊢ ↑a < ↑b ↔ ↑a ≤ ↑b ∧ ¬↑b ≤ ↑a
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
(choice (PosNum.transfer_rw "transfer_rw") (Num.transfer_rw "transfer_rw"))

Goal state after:
α : Type u_1
a b : PosNum
⊢ ↑a ≤ ↑b → ↑b ≤ ↑a → ↑a = ↑b
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
a b : PosNum
⊢ a ≤ b ∨ b ≤ a

Tactic:
(choice (PosNum.transfer_rw "transfer_rw") (Num.transfer_rw "transfer_rw"))

Goal state after:
α : Type u_1
a b : PosNum
⊢ ↑a ≤ ↑b ∨ ↑b ≤ ↑a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case false
n : Num
⊢ ↑(bit false n) = Nat.bit false ↑n

Tactic:
cases n

Goal state after:
case false.zero
⊢ ↑(bit false zero) = Nat.bit false ↑zero

case false.pos
a✝ : PosNum
⊢ ↑(bit false (pos a✝)) = Nat.bit false ↑(pos a✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case true
n : Num
⊢ ↑(bit true n) = Nat.bit true ↑n

Tactic:
cases n

Goal state after:
case true.zero
⊢ ↑(bit true zero) = Nat.bit true ↑zero

case true.pos
a✝ : PosNum
⊢ ↑(bit true (pos a✝)) = Nat.bit true ↑(pos a✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : Num
⊢ -n.toZNum = n.toZNumNeg

Tactic:
cases n

Goal state after:
case zero
⊢ -zero.toZNum = zero.toZNumNeg

case pos
a✝ : PosNum
⊢ -(pos a✝).toZNum = (pos a✝).toZNumNeg
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : Num
⊢ -n.toZNumNeg = n.toZNum

Tactic:
cases n

Goal state after:
case zero
⊢ -zero.toZNumNeg = zero.toZNum

case pos
a✝ : PosNum
⊢ -(pos a✝).toZNumNeg = (pos a✝).toZNum
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : Num
h : zero.toZNum = n.toZNum
⊢ zero = n

Tactic:
cases n

Goal state after:
case zero.zero
h : zero.toZNum = zero.toZNum
⊢ zero = zero

case zero.pos
a✝ : PosNum
h : zero.toZNum = (pos a✝).toZNum
⊢ zero = pos a✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos
n : Num
a✝ : PosNum
h : (pos a✝).toZNum = n.toZNum
⊢ pos a✝ = n

Tactic:
cases n

Goal state after:
case pos.zero
a✝ : PosNum
h : (pos a✝).toZNum = zero.toZNum
⊢ pos a✝ = zero

case pos.pos
a✝¹ a✝ : PosNum
h : (pos a✝¹).toZNum = (pos a✝).toZNum
⊢ pos a✝¹ = pos a✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : Num
⊢ (zero + n).toZNum = zero.toZNum + n.toZNum

Tactic:
cases n

Goal state after:
case zero.zero
⊢ (zero + zero).toZNum = zero.toZNum + zero.toZNum

case zero.pos
a✝ : PosNum
⊢ (zero + pos a✝).toZNum = zero.toZNum + (pos a✝).toZNum
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos
n : Num
a✝ : PosNum
⊢ (pos a✝ + n).toZNum = (pos a✝).toZNum + n.toZNum

Tactic:
cases n

Goal state after:
case pos.zero
a✝ : PosNum
⊢ (pos a✝ + zero).toZNum = (pos a✝).toZNum + zero.toZNum

case pos.pos
a✝¹ a✝ : PosNum
⊢ (pos a✝¹ + pos a✝).toZNum = (pos a✝¹).toZNum + (pos a✝).toZNum
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ ↑zero
⊢ ↑(Num.casesOn zero 1 id) = (↑n).pred

Tactic:
exact absurd this (by decide)

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

Goal state before:
pp: case zero
n : Num
⊢ (zero.cmp n).swap = n.cmp zero

Tactic:
cases n

Goal state after:
case zero.zero
⊢ (zero.cmp zero).swap = zero.cmp zero

case zero.pos
a✝ : PosNum
⊢ (zero.cmp (pos a✝)).swap = (pos a✝).cmp zero
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos
n : Num
a✝ : PosNum
⊢ ((pos a✝).cmp n).swap = n.cmp (pos a✝)

Tactic:
cases n

Goal state after:
case pos.zero
a✝ : PosNum
⊢ ((pos a✝).cmp zero).swap = zero.cmp (pos a✝)

case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)
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 : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
h : (cf.eval n).Dom ∨ (cg.eval n).Dom
⊢ (rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n).Dom

Tactic:
rw [Nat.rfindOpt_dom]

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 : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
h : (cf.eval n).Dom ∨ (cg.eval n).Dom
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Partrec' fun v ↦ f v.head

Tactic:
obtain ⟨c, rfl⟩ := exists_code.1 hf

Goal state after:
c : Partrec.Code
hf : Nat.Partrec c.eval
⊢ Partrec' fun v ↦ c.eval v.head
Module: Mathlib.Computability.TuringMachine.Tape

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

Tactic:
simp only [← List.replicate_add, Nat.add_sub_cancel' h, List.append_assoc]

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

Goal state before:
pp: case refine_1
Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : l₁.length ≤ l₂.length
h' : BlankExtends l₂ l₁
⊢ BlankExtends l₁ l₂

Tactic:
exact (BlankExtends.refl _).above_of_le h' hl

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

Goal state before:
pp: Γ : Type ?u.6
inst✝ : Inhabited Γ
a : Γ
l : ListBlank Γ
⊢ ListBlank Γ

Tactic:
by
  apply l.liftOn (fun l ↦ ListBlank.mk (List.cons a l))
  rintro _ _ ⟨i, rfl⟩
  exact Quotient.sound' (Or.inl ⟨i, rfl⟩)

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
n : ℕ
L : ListBlank Γ
⊢ map F (modifyNth f n L) = modifyNth f' n (map F L)

Tactic:
induction n generalizing L <;>
    simp only [*, ListBlank.head_map, ListBlank.modifyNth, ListBlank.map_cons, ListBlank.tail_map]

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
n : ℕ
⊢ T.right₀.nth n = T.nth ↑n

Tactic:
cases n

Goal state after:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ T.right₀.nth 0 = T.nth ↑0

case succ
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
n✝ : ℕ
⊢ T.right₀.nth (n✝ + 1) = T.nth ↑(n✝ + 1)
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
x : α ⊕ β
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)

Tactic:
by cases x <;> [apply h₁; apply h₂]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ rmatch 0 x = false

Tactic:
induction x <;> simp [rmatch, matchEpsilon, *]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ rmatch 1 x = true ↔ x = []

Tactic:
induction x <;> simp [rmatch, matchEpsilon, *]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case pos.mpr.cons
α : 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
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ (P.deriv a).rmatch t = true

Tactic:
convert! hP

Goal state after:
α : 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
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
⊢ SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q

Tactic:
induction i generalizing q

Goal state after:
case zero
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S ((Stmt.move d)^[0] q) = SupportsStmt S q

case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
n✝ : ℕ
a✝ : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n✝] q) = SupportsStmt S q
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S ((Stmt.move d)^[n✝ + 1] q) = SupportsStmt S q
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg.mpr.cons
α : 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
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ (P.deriv a).rmatch t = true

Tactic:
convert! hP

Goal state after:
α : 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
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n (addBottom L) = addBottom (ListBlank.modifyNth f n L)

Tactic:
cases n

Goal state after:
case zero
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) 0 (addBottom L) = addBottom (ListBlank.modifyNth f 0 L)

case succ
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) (n✝ + 1) (addBottom L) = addBottom (ListBlank.modifyNth f (n✝ + 1) L)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: v : List ℕ
⊢ pred.eval v = pure [v.headI.pred]

Tactic:
simp [pred]

Goal state after:
v : List ℕ
⊢ Nat.rec (Part.some [0]) (fun y x ↦ Part.some [y]) v.headI = Part.some [v.headI - 1]
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg.inr
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
h : tl.length < i
⊢ ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.getI i

Tactic:
· rw [List.getI_eq_default, List.getI_eq_default] <;>
            simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
              List.length_append, List.length_map]

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

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

Tactic:
Cont.then

Goal state after:
case cons
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.cons₁ c' v (k.then k')) v = stepNormal c ((fun k' ↦ Cont.cons₁ c' v (k.then k')) k') v