mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.one.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
n : PosNum
⊢ ↑(p 1 (PosNum.bit false n)) = Nat.bit (g true false) (Nat.bitwise g 0 ↑n)

Tactic:
]

Goal state after:
case pos.pos.one.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
n : PosNum
⊢ ↑(p 1 (PosNum.bit false n)) = Nat.bit (g true false) (Nat.bitwise g 0 ↑n)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f (cons l.head l.tail)).head = f.f (cons l.head l.tail).head

Tactic:
]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f (cons l.head l.tail)).head = f.f (cons l.head l.tail).head
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit1.one
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
⊢ ↑(p (PosNum.bit true m) 1) = Nat.bitwise g (Nat.bit true ↑m) (Nat.bit true 0)

Tactic:
]

Goal state after:
case pos.pos.bit1.one
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
⊢ ↑(p (PosNum.bit true m) 1) = Nat.bitwise g (Nat.bit true ↑m) (Nat.bit true 0)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f (cons l.head l.tail)).tail = map f (cons l.head l.tail).tail

Tactic:
]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f (cons l.head l.tail)).tail = map f (cons l.head l.tail).tail
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (List.map f.f l).getD n default = (List.map f.f l).getD n (f.f default)

Tactic:
]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (List.map f.f l).getD n default = (List.map f.f l).getD n (f.f default)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (proj i).f (L.nth n) = L.nth n i

Tactic:
]

Goal state after:
ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (proj i).f (L.nth n) = L.nth n i
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit1.one
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
⊢ ↑(p (PosNum.bit true m) 1) = Nat.bit (g true true) (Nat.bitwise g (↑m) 0)

Tactic:
]

Goal state after:
case pos.pos.bit1.one
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
⊢ ↑(p (PosNum.bit true m) 1) = Nat.bit (g true true) (Nat.bitwise g (↑m) 0)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ List.flatMap f l ++ List.flatMap f (List.replicate i default) = List.flatMap f l ++ List.replicate (n * i) default

Tactic:
]

Goal state after:
Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ List.flatMap f l ++ List.flatMap f (List.replicate i default) = List.flatMap f l ++ List.replicate (n * i) default
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit1.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit true n)) = Nat.bitwise g (Nat.bit true ↑m) ↑(pos (PosNum.bit true n))

Tactic:
]

Goal state after:
case pos.pos.bit1.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit true n)) = Nat.bitwise g (Nat.bit true ↑m) ↑(pos (PosNum.bit true n))
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
L R : ListBlank Γ
n : ℕ
⊢ R.nth n = R.nth n

Tactic:
]

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

Goal state before:
pp: case pos.pos.bit1.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit true n)) = Nat.bitwise g (Nat.bit true ↑m) (Nat.bit true ↑n)

Tactic:
]

Goal state after:
case pos.pos.bit1.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit true n)) = Nat.bitwise g (Nat.bit true ↑m) (Nat.bit true ↑n)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) =
    { head := a, left := L, right := R }.nth ↑(n + 1)

Tactic:
]

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) =
    { head := a, left := L, right := R }.nth ↑(n + 1)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ R.nth n = R.nth n

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ (move Dir.right T).nth i = (move Dir.right T).nth i

Tactic:
]

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

Goal state before:
pp: case pos.pos.bit1.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit true n)) = Nat.bit (g true true) (Nat.bitwise g ↑m ↑n)

Tactic:
]

Goal state after:
case pos.pos.bit1.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit true n)) = Nat.bit (g true true) (Nat.bitwise g ↑m ↑n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit1.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit false n)) = Nat.bitwise g (Nat.bit true ↑m) ↑(pos (PosNum.bit false n))

Tactic:
]

Goal state after:
case pos.pos.bit1.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit false n)) = Nat.bitwise g (Nat.bit true ↑m) ↑(pos (PosNum.bit false n))
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ Nat.RecursiveIn O g

Tactic:
]

Goal state after:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ Nat.RecursiveIn O g
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
s : Part ℕ
hf : RecursiveIn {fun x ↦ s} f
g : ℕ →. ℕ
hg : g ∈ {fun x ↦ s}
⊢ Partrec fun x ↦ s

Tactic:
]

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
s : Part ℕ
hf : RecursiveIn {fun x ↦ s} f
g : ℕ →. ℕ
hg : g ∈ {fun x ↦ s}
⊢ Partrec fun x ↦ s
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit1.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit false n)) = Nat.bitwise g (Nat.bit true ↑m) (Nat.bit false ↑n)

Tactic:
]

Goal state after:
case pos.pos.bit1.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit false n)) = Nat.bitwise g (Nat.bit true ↑m) (Nat.bit false ↑n)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case none
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
e : step M c = none
⊢ match none with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => Option.map (Cfg.map f₁ g₁.f) none = none

Tactic:
]

Goal state after:
case none
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
e : step M c = none
⊢ match none with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => Option.map (Cfg.map f₁ g₁.f) none = none