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

Goal state before:
pp: n : ℕ
⊢ (fun b ↦ succ.comp (n, b).2)^[id n] zero = Code.const n

Tactic:
simp

Goal state after:
n : ℕ
⊢ (fun b ↦ succ.comp b)^[n] zero = Code.const n
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
i : α
this : ↑n₀ / b' ≤ ↑n
⊢ ↑n₀ ≤ b' * ↑n

Tactic:
div_le_iff₀,

Goal state after:
α : 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
i : α
this : ↑n₀ ≤ ↑n * b'
⊢ ↑n₀ ≤ b' * ↑n

α : 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
i : α
this : ↑n₀ / b' ≤ ↑n
⊢ 0 < b'
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x : ℕ
⊢ ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m x_1)) = some x →
        ∃
          a ∈
            Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
              m,
          x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m a))

Tactic:
| succ m IH =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case prec.succ
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n₁ m : ℕ
IH :
  ∀ {n x : ℕ},
    x ∈ Nat.rec (cf.eval n₁) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m →
      ∃ k,
        n ≤ k ∧
          Nat.rec (evaln (k + 1) cf n₁)
              (fun n n_ih ↦
                (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun i ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
              m =
            some x
n x : ℕ
⊢ ∀ x_1 ∈ Nat.rec (cf.eval n₁) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m,
    x ∈ cg.eval (Nat.pair n₁ (Nat.pair m x_1)) →
      ∃ k,
        n ≤ k ∧
          ∃ a, evaln k (cf.prec cg) (Nat.pair n₁ m) = some a ∧ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair m a)) = some x

Tactic:
| succ m IH =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

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

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case zero
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l ^ 0 ↔ ∃ S, x = S.flatten ∧ S.length = 0 ∧ ∀ y ∈ S, y ∈ l

Tactic:
simp

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 α
a : Language α
x✝ : List α
hl : x✝ ∈ 1
⊢ ∀ y ∈ [], y ∈ a

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Language

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

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Language

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

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v s : List (Symbol T N)
⊢ Symbol.nonterminal r.input :: s = [] ++ [Symbol.nonterminal r.input] ++ s ∧ r.output ++ s = [] ++ r.output ++ s

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
p' q' : List (Symbol T N)
hrs✝ : r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q')
⊢ x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = x :: p' ++ [Symbol.nonterminal r.input] ++ q' ∧
    x :: (p' ++ r.output ++ q') = x :: p' ++ r.output ++ q'

Tactic:
simp

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:
by
  induction p with
  | nil => exact Rewrites.head q
  | cons d l ih => exact Rewrites.cons d ih

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
x✝ : ContextFreeRule T N
⊢ (reverse ∘ reverse) x✝ = id x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case e'_2
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
⊢ g = g.reverse.reverse

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case e'_3
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
e_2✝ : g = g.reverse.reverse
⊢ u = u.reverse.reverse

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case e'_4
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
e_2✝ : g = g.reverse.reverse
⊢ v = v.reverse.reverse

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
x✝ : List T
⊢ x✝ ∈ g.reverse.language ↔ x✝ ∈ g.language.reverse

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
⊢ g.reverse.language = g.language.reverse

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
⊢ Fintype.card σ < Fintype.card (Fin (Fintype.card σ + 1))

Tactic:
simp

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ 1 > 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ (fun n ↦ 1 * asympBound g a b n) = asympBound g a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ asympBound g a b = fun n ↦ 1 * asympBound g a b n

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
s : σ
⊢ (comap f M).evalFrom s [] = M.evalFrom s (List.map f [])

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M✝ : DFA α σ
α' : Type u_1
σ' : Type u_2
g : σ ≃ σ'
M : DFA α σ
⊢ (fun M ↦ { step := fun s a ↦ g.symm (M.step (g s) a), start := g.symm M.start, accept := ⇑g ⁻¹' M.accept })
      ((fun M ↦ { step := fun s a ↦ g (M.step (g.symm s) a), start := g M.start, accept := ⇑g.symm ⁻¹' M.accept }) M) =
    M

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M✝ : DFA α σ
α' : Type u_1
σ' : Type u_2
g : σ ≃ σ'
M : DFA α σ'
⊢ (fun M ↦ { step := fun s a ↦ g (M.step (g.symm s) a), start := g M.start, accept := ⇑g.symm ⁻¹' M.accept })
      ((fun M ↦ { step := fun s a ↦ g.symm (M.step (g s) a), start := g.symm M.start, accept := ⇑g ⁻¹' M.accept }) M) =
    M

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
s : σ'
⊢ ((reindex g) M).evalFrom s [] = g (M.evalFrom (g.symm s) [])

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case nil
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
⊢ (M1.union M2).evalFrom (s1, s2) [] ∈ (M1.union M2).accept ↔
    M1.evalFrom s1 [] ∈ M1.accept ∨ M2.evalFrom s2 [] ∈ M2.accept

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case nil
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
⊢ (M1.inter M2).evalFrom (s1, s2) [] ∈ (M1.inter M2).accept ↔
    M1.evalFrom s1 [] ∈ M1.accept ∧ M2.evalFrom s2 [] ∈ M2.accept

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ 0 < 2 ^ size 0

Tactic:
simp

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

Goal state before:
pp: case false.false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if false = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if false = true then 2 * n + 1 else 2 * n else 0
    else
      if (if false = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if false = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if false = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if false = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2)) =
    if f false false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
simp

Goal state after:
case false.false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if m = 0 then if f false true = true then 2 * n else 0
    else
      if n = 0 then if f true false = true then 2 * m else 0
      else if f false false = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    if f false false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case false.true
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if false = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if true = true then 2 * n + 1 else 2 * n else 0
    else
      if (if true = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if false = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if false = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if true = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if true = true then 2 * n + 1 else 2 * n) / 2)) =
    if f false true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
simp

Goal state after:
case false.true
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if m = 0 then if f false true = true then 2 * n + 1 else 0
    else
      if f false true = true then bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) + 1
      else bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2)) =
    if f false true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case true.false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if true = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if false = true then 2 * n + 1 else 2 * n else 0
    else
      if (if false = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if true = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if true = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if false = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if false = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2)) =
    if f true false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
simp

Goal state after:
case true.false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if n = 0 then if f true false = true then 2 * m + 1 else 0
    else
      if f true false = true then bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n + 1
      else bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n) =
    if f true false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case true.true
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if true = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if true = true then 2 * n + 1 else 2 * n else 0
    else
      if (if true = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if true = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if true = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if true = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
                ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
              ((if true = true then 2 * n + 1 else 2 * n) / 2)) =
    if f true true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
simp

Goal state after:
case true.true
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if f true true = true then
      bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1
    else bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2)) =
    if f true true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case zero
n : ℕ
h : 0 < 2 ^ n
⊢ size 0 ≤ n

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ (bits 0).length = size 0

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝ : Unit
p n : ℕ
⊢ List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: n : ℕ
h : ∀ (i : ℕ), n.testBit i = false
⊢ n = 0

Tactic:
induction n using Nat.binaryRec with | zero => rfl | bit b n hn => ?_
  have : b = false := by simpa using h 0
  rw [this, bit_false, hn fun i => by rw [← h (i + 1), testBit_bit_succ]]

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

Goal state before:
pp: case succ.nil
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ [].tail.getI i = [].getI (i + 1)

Tactic:
simp

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

Goal state before:
pp: case succ.cons
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
head✝ : Bool
tail✝ : List Bool
⊢ (head✝ :: tail✝).tail.getI i = (head✝ :: tail✝).getI (i + 1)

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero
f : Bool → Bool → Bool
n : ℕ
⊢ bitwise (swap f) 0 n = bitwise f n 0

Tactic:
simp

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

Goal state before:
pp: case bit.zero
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap f) m n = bitwise f n m
⊢ bitwise (swap f) (bit bm m) 0 = bitwise f 0 (bit bm m)

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (0 + 1)) =
    match Fin.ofNat 4 0 with
    | 0 => 0
    | 1 => 1
    | 2 => 0 + 1
    | 3 => 0

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.rfind'.some.zero
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ Nat.rec (some (unpair n).2)
      (fun n_1 n_ih ↦
        lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      0 =
    if 0 = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.rfind'.some.succ
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
n✝ : ℕ
⊢ Nat.rec (some (unpair n).2)
      (fun n_1 n_ih ↦
        lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      (n✝ + 1) =
    if n✝ + 1 = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))

Tactic:
simp

Goal state after:
case succ.rfind'.some.succ
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
n✝ : ℕ
⊢ lup
      (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
        (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
      (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)) =
    evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ 2 ∣ 4

Tactic:
simp

Goal state after: