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

Goal state before:
pp: case inl
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ ∅ ↔ cg ∈ ∅)
hC : ∀ (f : Code), f ∈ ∅ ↔ f.eval ∈ eval '' ∅
⊢ ComputablePred fun c ↦ c ∈ ∅

pp: case inr
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ Set.univ ↔ cg ∈ Set.univ)
hC : ∀ (f : Code), f ∈ Set.univ ↔ f.eval ∈ eval '' Set.univ
⊢ ComputablePred fun c ↦ c ∈ Set.univ

Tactic:
<;>

Goal state after:
case inl
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ ∅ ↔ cg ∈ ∅)
hC : ∀ (f : Code), f ∈ ∅ ↔ f.eval ∈ eval '' ∅
⊢ ComputablePred fun c ↦ c ∈ ∅

case inr
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ Set.univ ↔ cg ∈ Set.univ)
hC : ∀ (f : Code), f ∈ Set.univ ↔ f.eval ∈ eval '' Set.univ
⊢ ComputablePred fun c ↦ c ∈ Set.univ
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
⊢ -zero.toZNum = zero.toZNumNeg

pp: case pos
a✝ : PosNum
⊢ -(pos a✝).toZNum = (pos a✝).toZNumNeg

Tactic:
<;>

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: case zero
⊢ -zero.toZNumNeg = zero.toZNum

pp: case pos
a✝ : PosNum
⊢ -(pos a✝).toZNumNeg = (pos a✝).toZNum

Tactic:
<;>

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

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

Tactic:
<;>

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

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

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

pp: case zero.pos
a✝ : PosNum
h : zero.toZNum = (pos a✝).toZNum
⊢ zero = pos a✝

pp: case pos.zero
a✝ : PosNum
h : (pos a✝).toZNum = zero.toZNum
⊢ pos a✝ = zero

pp: case pos.pos
a✝¹ a✝ : PosNum
h : (pos a✝¹).toZNum = (pos a✝).toZNum
⊢ pos a✝¹ = pos a✝

Tactic:
<;>

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✝

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.zero.refl
⊢ zero = zero

pp: case pos.pos.refl
a✝ : PosNum
⊢ pos a✝ = pos a✝

Tactic:
<;>

Goal state after:
case zero.zero.refl
⊢ zero = zero

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

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

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

Tactic:
<;>

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

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

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

pp: case zero.pos
a✝ : PosNum
⊢ (zero + pos a✝).toZNum = zero.toZNum + (pos a✝).toZNum

pp: case pos.zero
a✝ : PosNum
⊢ (pos a✝ + zero).toZNum = (pos a✝).toZNum + zero.toZNum

pp: case pos.pos
a✝¹ a✝ : PosNum
⊢ (pos a✝¹ + pos a✝).toZNum = (pos a✝¹).toZNum + (pos a✝).toZNum

Tactic:
<;>

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

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 one
⊢ one.sub' 1 = one.pred'.toZNum

pp: case bit1
a✝ : PosNum
⊢ a✝.bit1.sub' 1 = a✝.bit1.pred'.toZNum

pp: case bit0
a✝ : PosNum
⊢ a✝.bit0.sub' 1 = a✝.bit0.pred'.toZNum

Tactic:
<;>

Goal state after:
case one
⊢ one.sub' 1 = one.pred'.toZNum

case bit1
a✝ : PosNum
⊢ a✝.bit1.sub' 1 = a✝.bit1.pred'.toZNum

case bit0
a✝ : PosNum
⊢ a✝.bit0.sub' 1 = a✝.bit0.pred'.toZNum
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one
⊢ sub' 1 one = one.pred'.toZNumNeg

pp: case bit1
a✝ : PosNum
⊢ sub' 1 a✝.bit1 = a✝.bit1.pred'.toZNumNeg

pp: case bit0
a✝ : PosNum
⊢ sub' 1 a✝.bit0 = a✝.bit0.pred'.toZNumNeg

Tactic:
<;>

Goal state after:
case one
⊢ sub' 1 one = one.pred'.toZNumNeg

case bit1
a✝ : PosNum
⊢ sub' 1 a✝.bit1 = a✝.bit1.pred'.toZNumNeg

case bit0
a✝ : PosNum
⊢ sub' 1 a✝.bit0 = a✝.bit0.pred'.toZNumNeg
Module: Mathlib.Data.Num.Lemmas

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

pp: case eq
m n : PosNum
⊢ Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt

pp: case gt
m n : PosNum
⊢ Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt

Tactic:
<;>

Goal state after:
case lt
m n : PosNum
⊢ Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt

case eq
m n : PosNum
⊢ Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt

case gt
m n : PosNum
⊢ Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt
Module: Mathlib.Data.Num.Lemmas

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

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

Tactic:
<;>

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

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

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

pp: case zero.pos
a✝ : PosNum
⊢ (zero.cmp (pos a✝)).swap = (pos a✝).cmp zero

pp: case pos.zero
a✝ : PosNum
⊢ ((pos a✝).cmp zero).swap = zero.cmp (pos a✝)

pp: case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)

Tactic:
<;>

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

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.Data.Num.Lemmas

Goal state before:
pp: case lt
m n : Num
⊢ Ordering.casesOn Ordering.lt (m < n) (m = n) (n < m) → (Ordering.lt = Ordering.eq ↔ m = n)

pp: case eq
m n : Num
⊢ Ordering.casesOn Ordering.eq (m < n) (m = n) (n < m) → (Ordering.eq = Ordering.eq ↔ m = n)

pp: case gt
m n : Num
⊢ Ordering.casesOn Ordering.gt (m < n) (m = n) (n < m) → (Ordering.gt = Ordering.eq ↔ m = n)

Tactic:
<;>

Goal state after:
case lt
m n : Num
⊢ Ordering.casesOn Ordering.lt (m < n) (m = n) (n < m) → (Ordering.lt = Ordering.eq ↔ m = n)

case eq
m n : Num
⊢ Ordering.casesOn Ordering.eq (m < n) (m = n) (n < m) → (Ordering.eq = Ordering.eq ↔ m = n)

case gt
m n : Num
⊢ Ordering.casesOn Ordering.gt (m < n) (m = n) (n < m) → (Ordering.gt = Ordering.eq ↔ m = n)
Module: Mathlib.Data.Num.Lemmas

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

pp: case eq
m n : Num
⊢ Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt

pp: case gt
m n : Num
⊢ Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt

Tactic:
<;>

Goal state after:
case lt
m n : Num
⊢ Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt

case eq
m n : Num
⊢ Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt

case gt
m n : Num
⊢ Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt
Module: Mathlib.Data.Num.Lemmas

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

pp: case pos
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)
n : Num
m : PosNum
⊢ ↑(f (pos m) n) = Nat.bitwise g ↑(pos m) ↑n

Tactic:
<;>

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

case pos
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)
n : Num
m : PosNum
⊢ ↑(f (pos m) n) = Nat.bitwise g ↑(pos m) ↑n
Module: Mathlib.Computability.RE

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

pp: case inr
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e : x ∈ Code.evaln k cg n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
<;>

Goal state after:
case inl
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e : x ∈ Code.evaln k cf n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

case inr
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e : x ∈ Code.evaln k cg n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_1.e_a.zero
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ 0)) = ↑(some (ofNat (Option ℕ) 0).isSome)

pp: case refine_1.e_a.succ
n✝¹ : ℕ
f : List.Vector ℕ (n✝¹ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝¹
b a n n✝ : ℕ
⊢ Part.some (decide (1 ≤ n✝ + 1)) = ↑(some (ofNat (Option ℕ) (n✝ + 1)).isSome)

Tactic:
<;>

Goal state after:
case refine_1.e_a.zero
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ 0)) = ↑(some (ofNat (Option ℕ) 0).isSome)

case refine_1.e_a.succ
n✝¹ : ℕ
f : List.Vector ℕ (n✝¹ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝¹
b a n n✝ : ℕ
⊢ Part.some (decide (1 ≤ n✝ + 1)) = ↑(some (ofNat (Option ℕ) (n✝ + 1)).isSome)
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_1.e_a.zero
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝
b a n : ℕ
⊢ ofNat (Option ℕ) 0 = none

pp: case refine_1.e_a.succ
n✝¹ : ℕ
f : List.Vector ℕ (n✝¹ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝¹
b a n n✝ : ℕ
⊢ (ofNat (Option ℕ) (n✝ + 1)).isSome = true

Tactic:
<;>

Goal state after:
case refine_1.e_a.zero
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝
b a n : ℕ
⊢ ofNat (Option ℕ) 0 = none

case refine_1.e_a.succ
n✝¹ : ℕ
f : List.Vector ℕ (n✝¹ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝¹
b a n n✝ : ℕ
⊢ (ofNat (Option ℕ) (n✝ + 1)).isSome = true
Module: Mathlib.Computability.RE

Goal state before:
pp: case inl
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : decode (encode a') = Option.some x
⊢ x ∈ f a ∨ x ∈ g a

pp: case inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : decode (encode a') = Option.some x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : decode (encode a') = Option.some x
⊢ x ∈ f a ∨ x ∈ g a

case inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : decode (encode a') = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
Module: Mathlib.Computability.RE

Goal state before:
pp: case inl
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

pp: case inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

case inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero.pos.false
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)
n : PosNum
⊢ ↑(bif false then pos n else 0) = if false = true then ↑(pos n) else 0

pp: case zero.pos.true
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)
n : PosNum
⊢ ↑(bif true then pos n else 0) = if true = true then ↑(pos n) else 0

Tactic:
<;>

Goal state after:
case zero.pos.false
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)
n : PosNum
⊢ ↑(bif false then pos n else 0) = if false = true then ↑(pos n) else 0

case zero.pos.true
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)
n : PosNum
⊢ ↑(bif true then pos n else 0) = if true = true then ↑(pos n) else 0