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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
g : β → α → α
hg : Primrec₂ g
b : β
⊢ (List.casesOn ([], b).1 [] fun b_1 l ↦ g (([], b), b_1, l).1.2 (([], b), b_1, l).2.1 :: (([], b), b_1, l).2.2) =
    List.modifyHead (g b) []

pp: case cons
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
g : β → α → α
hg : Primrec₂ g
b : β
head✝ : α
tail✝ : List α
⊢ (List.casesOn (head✝ :: tail✝, b).1 [] fun b_1 l ↦
      g ((head✝ :: tail✝, b), b_1, l).1.2 ((head✝ :: tail✝, b), b_1, l).2.1 :: ((head✝ :: tail✝, b), b_1, l).2.2) =
    List.modifyHead (g b) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
g : β → α → α
hg : Primrec₂ g
b : β
⊢ (List.casesOn ([], b).1 [] fun b_1 l ↦ g (([], b), b_1, l).1.2 (([], b), b_1, l).2.1 :: (([], b), b_1, l).2.2) =
    List.modifyHead (g b) []

case cons
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
g : β → α → α
hg : Primrec₂ g
b : β
head✝ : α
tail✝ : List α
⊢ (List.casesOn (head✝ :: tail✝, b).1 [] fun b_1 l ↦
      g ((head✝ :: tail✝, b), b_1, l).1.2 ((head✝ :: tail✝, b), b_1, l).2.1 :: ((head✝ :: tail✝, b), b_1, l).2.2) =
    List.modifyHead (g b) (head✝ :: tail✝)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val✝ : β
⊢ Sum.casesOn (Sum.casesOn (Sum.inl val✝) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2)
      (fun b ↦ Part.some (h a b)) (g a) =
    Sum.casesOn (Sum.inl val✝) (g a) fun c ↦ Part.some (h a c)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val✝ : γ
⊢ Sum.casesOn (Sum.casesOn (Sum.inr val✝) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2)
      (fun b ↦ Part.some (h a b)) (g a) =
    Sum.casesOn (Sum.inr val✝) (g a) fun c ↦ Part.some (h a c)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val✝ : β
⊢ Sum.casesOn (Sum.casesOn (Sum.inl val✝) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2)
      (fun b ↦ Part.some (h a b)) (g a) =
    Sum.casesOn (Sum.inl val✝) (g a) fun c ↦ Part.some (h a c)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val✝ : γ
⊢ Sum.casesOn (Sum.casesOn (Sum.inr val✝) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2)
      (fun b ↦ Part.some (h a b)) (g a) =
    Sum.casesOn (Sum.inr val✝) (g a) fun c ↦ Part.some (h a c)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_1.zero
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
h₂ : Sum.inl b ∈ F a 0
_x : ∃ b', Sum.inl b' ∈ F a 0
h₁ : ∀ {m : ℕ}, m < 0 → ∃ b, Sum.inr b ∈ F a m
⊢ b ∈ f.fix a

pp: case refine_1.succ
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
n✝ : ℕ
h₂ : Sum.inl b ∈ F a (n✝ + 1)
_x : ∃ b', Sum.inl b' ∈ F a (n✝ + 1)
h₁ : ∀ {m : ℕ}, m < n✝ + 1 → ∃ b, Sum.inr b ∈ F a m
⊢ b ∈ f.fix a

Tactic:
<;>

Goal state after:
case refine_1.zero
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
h₂ : Sum.inl b ∈ F a 0
_x : ∃ b', Sum.inl b' ∈ F a 0
h₁ : ∀ {m : ℕ}, m < 0 → ∃ b, Sum.inr b ∈ F a m
⊢ b ∈ f.fix a

case refine_1.succ
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
n✝ : ℕ
h₂ : Sum.inl b ∈ F a (n✝ + 1)
_x : ∃ b', Sum.inl b' ∈ F a (n✝ + 1)
h₁ : ∀ {m : ℕ}, m < n✝ + 1 → ∃ b, Sum.inr b ∈ F a m
⊢ b ∈ f.fix a
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
n : ℕ
x✝ : List.Vector α n
h : [].length = n
⊢ (List.Vector.toList ⟨[], h⟩).tail = (List.Vector.tail ⟨[], h⟩).toList

pp: case cons
α : Type u_1
inst✝ : Primcodable α
n : ℕ
x✝ : List.Vector α n
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length = n
⊢ (List.Vector.toList ⟨head✝ :: tail✝, h⟩).tail = (List.Vector.tail ⟨head✝ :: tail✝, h⟩).toList

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : Primcodable α
n : ℕ
x✝ : List.Vector α n
h : [].length = n
⊢ (List.Vector.toList ⟨[], h⟩).tail = (List.Vector.tail ⟨[], h⟩).toList

case cons
α : Type u_1
inst✝ : Primcodable α
n : ℕ
x✝ : List.Vector α n
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length = n
⊢ (List.Vector.toList ⟨head✝ :: tail✝, h⟩).tail = (List.Vector.tail ⟨head✝ :: tail✝, h⟩).toList
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
v : List.Vector ℕ n.succ
⊢ v.get 0 = v.head

Tactic:
simp [get_zero]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case zero
v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH ↦ y) 0 = 0 - 1

pp: case succ
v : List.Vector ℕ (Nat.succ 0)
n✝ : ℕ
⊢ Nat.rec 0 (fun y IH ↦ y) (n✝ + 1) = n✝ + 1 - 1

Tactic:
<;>

Goal state after:
case zero
v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH ↦ y) 0 = 0 - 1

case succ
v : List.Vector ℕ (Nat.succ 0)
n✝ : ℕ
⊢ Nat.rec 0 (fun y IH ↦ y) (n✝ + 1) = n✝ + 1 - 1
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case zero
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH ↦ IH + 1) 0 = 0 + v.tail.head

pp: case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec v.tail.head (fun y IH ↦ IH + 1) n✝ = n✝ + v.tail.head
⊢ Nat.rec v.tail.head (fun y IH ↦ IH + 1) (n✝ + 1) = n✝ + 1 + v.tail.head

Tactic:
<;>

Goal state after:
case zero
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH ↦ IH + 1) 0 = 0 + v.tail.head

case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec v.tail.head (fun y IH ↦ IH + 1) n✝ = n✝ + v.tail.head
⊢ Nat.rec v.tail.head (fun y IH ↦ IH + 1) (n✝ + 1) = n✝ + 1 + v.tail.head
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case zero
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH ↦ IH - 1) 0 = v.tail.head - 0

pp: case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec v.tail.head (fun y IH ↦ IH - 1) n✝ = v.tail.head - n✝
⊢ Nat.rec v.tail.head (fun y IH ↦ IH - 1) (n✝ + 1) = v.tail.head - (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH ↦ IH - 1) 0 = v.tail.head - 0

case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec v.tail.head (fun y IH ↦ IH - 1) n✝ = v.tail.head - n✝
⊢ Nat.rec v.tail.head (fun y IH ↦ IH - 1) (n✝ + 1) = v.tail.head - (n✝ + 1)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case zero
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH ↦ v.tail.head + IH) 0 = 0 * v.tail.head

pp: case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec 0 (fun y IH ↦ v.tail.head + IH) n✝ = n✝ * v.tail.head
⊢ Nat.rec 0 (fun y IH ↦ v.tail.head + IH) (n✝ + 1) = (n✝ + 1) * v.tail.head

Tactic:
<;>

Goal state after:
case zero
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH ↦ v.tail.head + IH) 0 = 0 * v.tail.head

case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec 0 (fun y IH ↦ v.tail.head + IH) n✝ = n✝ * v.tail.head
⊢ Nat.rec 0 (fun y IH ↦ v.tail.head + IH) (n✝ + 1) = (n✝ + 1) * v.tail.head
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case pos
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ f v - (f v).sqrt * (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).1

pp: case neg
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).1

Tactic:
<;>

Goal state after:
case pos
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ f v - (f v).sqrt * (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).1

case neg
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case false
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ (match false, n.div2.bodd with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind').encodeCode =
    bit false (bit n.div2.bodd n.div2.div2) + 4

pp: case true
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ (match true, n.div2.bodd with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind').encodeCode =
    bit true (bit n.div2.bodd n.div2.div2) + 4

Tactic:
<;>

Goal state after:
case false
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ (match false, n.div2.bodd with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind').encodeCode =
    bit false (bit n.div2.bodd n.div2.div2) + 4

case true
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ (match true, n.div2.bodd with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind').encodeCode =
    bit true (bit n.div2.bodd n.div2.div2) + 4
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case pos
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).2

pp: case neg
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ f v - (f v).sqrt * (f v).sqrt - (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).2

Tactic:
<;>

Goal state after:
case pos
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).2

case neg
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ f v - (f v).sqrt * (f v).sqrt - (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).2
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ m → List.Vector ℕ n
h : Vec f
⊢ Primrec f

Tactic:
simpa using Primrec.vector_ofFn fun i => to_prim (h i)

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case ha
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 1 ≤ 2

pp: case hmn
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 3 ≤ n + 3

Tactic:
<;>

Goal state after:
case ha
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 1 ≤ 2

case hmn
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 3 ≤ n + 3
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
⊢ ofNatCode zero.encodeCode = zero

pp: case succ
⊢ ofNatCode succ.encodeCode = succ

pp: case left
⊢ ofNatCode left.encodeCode = left

pp: case right
⊢ ofNatCode right.encodeCode = right

pp: case pair
a✝¹ a✝ : Code
a_ih✝¹ : ofNatCode a✝¹.encodeCode = a✝¹
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode (a✝¹.pair a✝).encodeCode = a✝¹.pair a✝

pp: case comp
a✝¹ a✝ : Code
a_ih✝¹ : ofNatCode a✝¹.encodeCode = a✝¹
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode (a✝¹.comp a✝).encodeCode = a✝¹.comp a✝

pp: case prec
a✝¹ a✝ : Code
a_ih✝¹ : ofNatCode a✝¹.encodeCode = a✝¹
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode (a✝¹.prec a✝).encodeCode = a✝¹.prec a✝

pp: case rfind'
a✝ : Code
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode a✝.rfind'.encodeCode = a✝.rfind'

Tactic:
<;>

Goal state after:
case zero
⊢ ofNatCode zero.encodeCode = zero

case succ
⊢ ofNatCode succ.encodeCode = succ

case left
⊢ ofNatCode left.encodeCode = left

case right
⊢ ofNatCode right.encodeCode = right

case pair
a✝¹ a✝ : Code
a_ih✝¹ : ofNatCode a✝¹.encodeCode = a✝¹
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode (a✝¹.pair a✝).encodeCode = a✝¹.pair a✝

case comp
a✝¹ a✝ : Code
a_ih✝¹ : ofNatCode a✝¹.encodeCode = a✝¹
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode (a✝¹.comp a✝).encodeCode = a✝¹.comp a✝

case prec
a✝¹ a✝ : Code
a_ih✝¹ : ofNatCode a✝¹.encodeCode = a✝¹
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode (a✝¹.prec a✝).encodeCode = a✝¹.prec a✝

case rfind'
a✝ : Code
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode a✝.rfind'.encodeCode = a✝.rfind'
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ.zero
a✝ : 0 ^ 2 ≤ 2 ^ (0 + 1) - 3
⊢ (0 + 1) ^ 2 ≤ 2 ^ (0 + 1 + 1) - 3

pp: case succ.succ
n✝ : ℕ
a✝ : (n✝ + 1) ^ 2 ≤ 2 ^ (n✝ + 1 + 1) - 3
⊢ (n✝ + 1 + 1) ^ 2 ≤ 2 ^ (n✝ + 1 + 1 + 1) - 3

Tactic:
<;>

Goal state after:
case succ.zero
a✝ : 0 ^ 2 ≤ 2 ^ (0 + 1) - 3
⊢ (0 + 1) ^ 2 ≤ 2 ^ (0 + 1 + 1) - 3

case succ.succ
n✝ : ℕ
a✝ : (n✝ + 1) ^ 2 ≤ 2 ^ (n✝ + 1 + 1) - 3
⊢ (n✝ + 1 + 1) ^ 2 ≤ 2 ^ (n✝ + 1 + 1 + 1) - 3
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
⊢ encode cf < encode (cf.pair cg) ∧ encode cg < encode (cf.pair cg)

Tactic:
by
  simp only [encodeCode_eq, encodeCode]
  have := Nat.mul_le_mul_right (Nat.pair cf.encodeCode cg.encodeCode) (by decide : 1 ≤ 2 * 2)
  rw [one_mul, mul_assoc] at this
  have := lt_of_le_of_lt this (lt_add_of_pos_right _ (by decide : 0 < 4))
  exact ⟨lt_of_le_of_lt (Nat.left_le_pair _ _) this, lt_of_le_of_lt (Nat.right_le_pair _ _) this⟩

Goal state after:
Module: Mathlib.Computability.Ackermann

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

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

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

Tactic:
<;>

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

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

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

Goal state before:
pp: case zero
this : Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t
⊢ pappAck 0 = Nat.rec succ (fun x c ↦ pappAck.step c) 0

pp: case succ
this : Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t
n✝ : ℕ
a✝ : pappAck n✝ = Nat.rec succ (fun x c ↦ pappAck.step c) n✝
⊢ pappAck (n✝ + 1) = Nat.rec succ (fun x c ↦ pappAck.step c) (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
this : Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t
⊢ pappAck 0 = Nat.rec succ (fun x c ↦ pappAck.step c) 0

case succ
this : Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t
n✝ : ℕ
a✝ : pappAck n✝ = Nat.rec succ (fun x c ↦ pappAck.step c) n✝
⊢ pappAck (n✝ + 1) = Nat.rec succ (fun x c ↦ pappAck.step c) (n✝ + 1)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ -↑(-↑⌊-logb 2 (x / x₀)⌋₊) ≤ -logb 2 (x / x₀)

Tactic:
simp only [Int.cast_neg, Int.cast_natCast, neg_neg]

Goal state after:
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ ↑⌊-logb 2 (x / x₀)⌋₊ ≤ -logb 2 (x / x₀)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ Tendsto (fun x ↦ 1 / log x / 1) atTop (𝓝 0)

Tactic:
simp only [one_div, div_one]

Goal state after:
⊢ Tendsto (fun x ↦ (log x)⁻¹) atTop (𝓝 0)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case hc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ x ^ p a b) x

pp: case hd
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1 - ε x) x

Tactic:
<;>

Goal state after:
case hc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ x ^ p a b) x

case hd
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1 - ε x) x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1) x - deriv ε x = (-deriv ε) x

pp: case hf
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1) x

pp: case hg
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ ε x

Tactic:
<;>

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1) x - deriv ε x = (-deriv ε) x

case hf
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1) x

case hg
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ ε x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1) x + deriv ε x = deriv ε x

pp: case hf
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1) x

pp: case hg
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ ε x

Tactic:
<;>

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1) x + deriv ε x = deriv ε x

case hf
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1) x

case hg
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ ε x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1) x - deriv ε x = -deriv ε x

pp: case hf
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1) x

pp: case hg
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ ε x

Tactic:
<;>

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1) x - deriv ε x = -deriv ε x

case hf
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1) x

case hg
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ ε x