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

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun a ↦ ¬p a
⊢ Computable fun a ↦ decide (p a)

Tactic:
obtain ⟨k, pk, hk⟩ :=
        Partrec.merge (h₁.map (Computable.const true).to₂) (h₂.map (Computable.const false).to₂)
        (by
          intro a x hx y hy
          simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
            and_true, exists_const] at hx hy
          cases hy.1 hx.1)
      refine Partrec.of_eq pk fun n => Part.eq_some_iff.2 ?_
      rw [hk]
      simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
        true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff]
      apply Decidable.em

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

Goal state before:
pp: case left
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ default ∈ Set.univ

Tactic:
intros

Goal state after:
case left
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ default ∈ Set.univ
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ ∀ {q : Λ} {a : Γ} {q' : Λ} {s : Stmt Γ}, (q', s) ∈ M q a → q ∈ Set.univ → q' ∈ Set.univ

Tactic:
intros

Goal state after:
case right
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
q✝ : Λ
a✝² : Γ
q'✝ : Λ
s✝ : Stmt Γ
a✝¹ : (q'✝, s✝) ∈ M q✝ a✝²
a✝ : q✝ ∈ Set.univ
⊢ q'✝ ∈ Set.univ
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ = branch p q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
| branch p q₁ q₂ IH₁ IH₂ =>

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

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ = branch p q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S q₁✝

Tactic:
| branch p q₁ q₂ IH₁ IH₂ =>

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

Goal state before:
pp: case right.some.some.branch
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.branch p q₁ q₂) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
| branch p q₁ q₂ IH₁ IH₂ =>

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

Goal state before:
pp: case gff
⊢ (false || false) = false

Tactic:
intros

Goal state after:
case gff
⊢ (false || false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ 0 ||| 0 = 0

Tactic:
intros

Goal state after:
case f00
⊢ 0 ||| 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n.one
⊢ 0 ||| pos one = bif false || true then pos one else 0

Tactic:
intros

Goal state after:
case f0n.one
⊢ 0 ||| pos one = bif false || true then pos one else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n.bit1
a✝ : PosNum
⊢ 0 ||| pos a✝.bit1 = bif false || true then pos a✝.bit1 else 0

Tactic:
intros

Goal state after:
case f0n.bit1
a✝ : PosNum
⊢ 0 ||| pos a✝.bit1 = bif false || true then pos a✝.bit1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n.bit0
a✝ : PosNum
⊢ 0 ||| pos a✝.bit0 = bif false || true then pos a✝.bit0 else 0

Tactic:
intros

Goal state after:
case f0n.bit0
a✝ : PosNum
⊢ 0 ||| pos a✝.bit0 = bif false || true then pos a✝.bit0 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0.one
⊢ pos one ||| 0 = bif true || false then pos one else 0

Tactic:
intros

Goal state after:
case fn0.one
⊢ pos one ||| 0 = bif true || false then pos one else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0.bit1
a✝ : PosNum
⊢ pos a✝.bit1 ||| 0 = bif true || false then pos a✝.bit1 else 0

Tactic:
intros

Goal state after:
case fn0.bit1
a✝ : PosNum
⊢ pos a✝.bit1 ||| 0 = bif true || false then pos a✝.bit1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0.bit0
a✝ : PosNum
⊢ pos a✝.bit0 ||| 0 = bif true || false then pos a✝.bit0 else 0

Tactic:
intros

Goal state after:
case fn0.bit0
a✝ : PosNum
⊢ pos a✝.bit0 ||| 0 = bif true || false then pos a✝.bit0 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.one.one
⊢ pos one ||| pos one = pos (one.lor one)

Tactic:
intros

Goal state after:
case fnn.one.one
⊢ pos one ||| pos one = pos (one.lor one)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.one.bit1
a✝ : PosNum
⊢ pos one ||| pos a✝.bit1 = pos (one.lor a✝.bit1)

Tactic:
intros

Goal state after:
case fnn.one.bit1
a✝ : PosNum
⊢ pos one ||| pos a✝.bit1 = pos (one.lor a✝.bit1)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.one.bit0
a✝ : PosNum
⊢ pos one ||| pos a✝.bit0 = pos (one.lor a✝.bit0)

Tactic:
intros

Goal state after:
case fnn.one.bit0
a✝ : PosNum
⊢ pos one ||| pos a✝.bit0 = pos (one.lor a✝.bit0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.bit1.one
a✝ : PosNum
⊢ pos a✝.bit1 ||| pos one = pos (a✝.bit1.lor one)

Tactic:
intros

Goal state after:
case fnn.bit1.one
a✝ : PosNum
⊢ pos a✝.bit1 ||| pos one = pos (a✝.bit1.lor one)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.bit1.bit1
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit1 ||| pos a✝.bit1 = pos (a✝¹.bit1.lor a✝.bit1)

Tactic:
intros

Goal state after:
case fnn.bit1.bit1
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit1 ||| pos a✝.bit1 = pos (a✝¹.bit1.lor a✝.bit1)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.bit1.bit0
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit1 ||| pos a✝.bit0 = pos (a✝¹.bit1.lor a✝.bit0)

Tactic:
intros

Goal state after:
case fnn.bit1.bit0
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit1 ||| pos a✝.bit0 = pos (a✝¹.bit1.lor a✝.bit0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.bit0.one
a✝ : PosNum
⊢ pos a✝.bit0 ||| pos one = pos (a✝.bit0.lor one)

Tactic:
intros

Goal state after:
case fnn.bit0.one
a✝ : PosNum
⊢ pos a✝.bit0 ||| pos one = pos (a✝.bit0.lor one)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.bit0.bit1
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit0 ||| pos a✝.bit1 = pos (a✝¹.bit0.lor a✝.bit1)

Tactic:
intros

Goal state after:
case fnn.bit0.bit1
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit0 ||| pos a✝.bit1 = pos (a✝¹.bit0.lor a✝.bit1)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.bit0.bit0
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit0 ||| pos a✝.bit0 = pos (a✝¹.bit0.lor a✝.bit0)

Tactic:
intros

Goal state after:
case fnn.bit0.bit0
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit0 ||| pos a✝.bit0 = pos (a✝¹.bit0.lor a✝.bit0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ pos (lor 1 1) = bif true || true then 1 else 0

Tactic:
intros

Goal state after:
case p11
⊢ pos (lor 1 1) = bif true || true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.false.one
⊢ pos (lor 1 (PosNum.bit false one)) = bit (true || false) (bif false || true then pos one else 0)

Tactic:
intros

Goal state after:
case p1b.false.one
⊢ pos (lor 1 (PosNum.bit false one)) = bit (true || false) (bif false || true then pos one else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.false.bit1
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit false a✝.bit1)) = bit (true || false) (bif false || true then pos a✝.bit1 else 0)

Tactic:
intros

Goal state after:
case p1b.false.bit1
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit false a✝.bit1)) = bit (true || false) (bif false || true then pos a✝.bit1 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.false.bit0
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit false a✝.bit0)) = bit (true || false) (bif false || true then pos a✝.bit0 else 0)

Tactic:
intros

Goal state after:
case p1b.false.bit0
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit false a✝.bit0)) = bit (true || false) (bif false || true then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.true.one
⊢ pos (lor 1 (PosNum.bit true one)) = bit (true || true) (bif false || true then pos one else 0)

Tactic:
intros

Goal state after:
case p1b.true.one
⊢ pos (lor 1 (PosNum.bit true one)) = bit (true || true) (bif false || true then pos one else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.true.bit1
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit true a✝.bit1)) = bit (true || true) (bif false || true then pos a✝.bit1 else 0)

Tactic:
intros

Goal state after:
case p1b.true.bit1
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit true a✝.bit1)) = bit (true || true) (bif false || true then pos a✝.bit1 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.true.bit0
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit true a✝.bit0)) = bit (true || true) (bif false || true then pos a✝.bit0 else 0)

Tactic:
intros

Goal state after:
case p1b.true.bit0
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit true a✝.bit0)) = bit (true || true) (bif false || true then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.false.one
⊢ pos ((PosNum.bit false one).lor 1) = bit (false || true) (bif true || false then pos one else 0)

Tactic:
intros

Goal state after:
case pb1.false.one
⊢ pos ((PosNum.bit false one).lor 1) = bit (false || true) (bif true || false then pos one else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.false.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit false a✝.bit1).lor 1) = bit (false || true) (bif true || false then pos a✝.bit1 else 0)

Tactic:
intros

Goal state after:
case pb1.false.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit false a✝.bit1).lor 1) = bit (false || true) (bif true || false then pos a✝.bit1 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.false.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit false a✝.bit0).lor 1) = bit (false || true) (bif true || false then pos a✝.bit0 else 0)

Tactic:
intros

Goal state after:
case pb1.false.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit false a✝.bit0).lor 1) = bit (false || true) (bif true || false then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.true.one
⊢ pos ((PosNum.bit true one).lor 1) = bit (true || true) (bif true || false then pos one else 0)

Tactic:
intros

Goal state after:
case pb1.true.one
⊢ pos ((PosNum.bit true one).lor 1) = bit (true || true) (bif true || false then pos one else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.true.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit1).lor 1) = bit (true || true) (bif true || false then pos a✝.bit1 else 0)

Tactic:
intros

Goal state after:
case pb1.true.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit1).lor 1) = bit (true || true) (bif true || false then pos a✝.bit1 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.true.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit0).lor 1) = bit (true || true) (bif true || false then pos a✝.bit0 else 0)

Tactic:
intros

Goal state after:
case pb1.true.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit0).lor 1) = bit (true || true) (bif true || false then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.false.false
⊢ ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit false n)) = bit (false || false) (pos (m.lor n))

Tactic:
intros

Goal state after:
case pbb.false.false
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit false m✝).lor (PosNum.bit false n✝)) = bit (false || false) (pos (m✝.lor n✝))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.false.true
⊢ ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit true n)) = bit (false || true) (pos (m.lor n))

Tactic:
intros

Goal state after:
case pbb.false.true
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit false m✝).lor (PosNum.bit true n✝)) = bit (false || true) (pos (m✝.lor n✝))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.true.false
⊢ ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit false n)) = bit (true || false) (pos (m.lor n))

Tactic:
intros

Goal state after:
case pbb.true.false
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit true m✝).lor (PosNum.bit false n✝)) = bit (true || false) (pos (m✝.lor n✝))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.true.true
⊢ ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit true n)) = bit (true || true) (pos (m.lor n))

Tactic:
intros

Goal state after:
case pbb.true.true
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit true m✝).lor (PosNum.bit true n✝)) = bit (true || true) (pos (m✝.lor n✝))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gff
⊢ (false && false) = false

Tactic:
intros

Goal state after:
case gff
⊢ (false && false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ 0 &&& 0 = 0

Tactic:
intros

Goal state after:
case f00
⊢ 0 &&& 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n
⊢ ∀ (n : PosNum), 0 &&& pos n = bif false && true then pos n else 0

Tactic:
intros

Goal state after:
case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0
⊢ ∀ (n : PosNum), pos n &&& 0 = bif true && false then pos n else 0

Tactic:
intros

Goal state after:
case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
⊢ ∀ (m n : PosNum), pos m &&& pos n = m.land n

Tactic:
intros

Goal state after:
case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

Tactic:
intros

Goal state after:
case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b
⊢ ∀ (b : Bool) (n : PosNum), PosNum.land 1 (PosNum.bit b n) = bit (true && b) (bif false && true then pos n else 0)

Tactic:
intros

Goal state after:
case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit b✝ n✝) = bit (true && b✝) (bif false && true then pos n✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
⊢ ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).land 1 = bit (a && true) (bif true && false then pos m else 0)

Tactic:
intros

Goal state after:
case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land 1 = bit (a✝ && true) (bif true && false then pos m✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)

Tactic:
intros

Goal state after:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land (PosNum.bit b✝ n✝) = bit (a✝ && b✝) (m✝.land n✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gff
⊢ (false && !false) = false

Tactic:
intros

Goal state after:
case gff
⊢ (false && !false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ ldiff 0 0 = 0

Tactic:
intros

Goal state after:
case f00
⊢ ldiff 0 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n
⊢ ∀ (n : PosNum), ldiff 0 (pos n) = bif false && !true then pos n else 0

Tactic:
intros

Goal state after:
case f0n
n✝ : PosNum
⊢ ldiff 0 (pos n✝) = bif false && !true then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0
⊢ ∀ (n : PosNum), (pos n).ldiff 0 = bif true && !false then pos n else 0

Tactic:
intros

Goal state after:
case fn0
n✝ : PosNum
⊢ (pos n✝).ldiff 0 = bif true && !false then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
⊢ ∀ (m n : PosNum), (pos m).ldiff (pos n) = m.ldiff n

Tactic:
intros

Goal state after:
case fnn
m✝ n✝ : PosNum
⊢ (pos m✝).ldiff (pos n✝) = m✝.ldiff n✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0

Tactic:
intros

Goal state after:
case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b
⊢ ∀ (b : Bool) (n : PosNum), PosNum.ldiff 1 (PosNum.bit b n) = bit (true && !b) (bif false && !true then pos n else 0)

Tactic:
intros

Goal state after:
case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit b✝ n✝) = bit (true && !b✝) (bif false && !true then pos n✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
⊢ ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).ldiff 1 = bit (a && !true) (bif true && !false then pos m else 0)

Tactic:
intros

Goal state after:
case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff 1 = bit (a✝ && !true) (bif true && !false then pos m✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)

Tactic:
intros

Goal state after:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff (PosNum.bit b✝ n✝) = bit (a✝ && !b✝) (m✝.ldiff n✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gff
⊢ (false != false) = false

Tactic:
intros

Goal state after:
case gff
⊢ (false != false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ 0 ^^^ 0 = 0

Tactic:
intros

Goal state after:
case f00
⊢ 0 ^^^ 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n
⊢ ∀ (n : PosNum), 0 ^^^ pos n = bif false != true then pos n else 0

Tactic:
intros

Goal state after:
case f0n
n✝ : PosNum
⊢ 0 ^^^ pos n✝ = bif false != true then pos n✝ else 0
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q₁) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q₁ v (Tape.mk' L R)))
IH₂ :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q₂) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q₂ v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.branch p q₁ q₂)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.branch p q₁ q₂) v (Tape.mk' L R)))

Tactic:
| branch p q₁ q₂ IH₁ IH₂ =>

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

Goal state before:
pp: case fn0
⊢ ∀ (n : PosNum), pos n ^^^ 0 = bif true != false then pos n else 0

Tactic:
intros

Goal state after:
case fn0
n✝ : PosNum
⊢ pos n✝ ^^^ 0 = bif true != false then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
⊢ ∀ (m n : PosNum), pos m ^^^ pos n = m.lxor n

Tactic:
intros

Goal state after:
case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0

Tactic:
intros

Goal state after:
case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b
⊢ ∀ (b : Bool) (n : PosNum), PosNum.lxor 1 (PosNum.bit b n) = bit (true != b) (bif false != true then pos n else 0)

Tactic:
intros

Goal state after:
case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit b✝ n✝) = bit (true != b✝) (bif false != true then pos n✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
⊢ ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).lxor 1 = bit (a != true) (bif true != false then pos m else 0)

Tactic:
intros

Goal state after:
case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).lxor 1 = bit (a✝ != true) (bif true != false then pos m✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)

Tactic:
intros

Goal state after:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).lxor (PosNum.bit b✝ n✝) = bit (a✝ != b✝) (m✝.lxor n✝)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  SupportsStmt S q₁ →
    (∀ q' ∈ writes q₁, q' ∈ trSupp M S) →
      SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
IH₂ :
  SupportsStmt S q₂ →
    (∀ q' ∈ writes q₂, q' ∈ trSupp M S) →
      SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ q' ∈ writes (Stmt.branch p q₁ q₂), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
    ∀ q' ∈ writes (Stmt.branch p q₁ q₂), SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
| branch p q₁ q₂ IH₁ IH₂ =>

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

Goal state before:
pp: case right.e_a.e_a.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ (tail✝.reverse ++ [head✝])[tail✝.length]? = (head✝ :: tail✝).head?

Tactic:
← List.length_reverse,

Goal state after:
case right.e_a.e_a.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ (tail✝.reverse ++ [head✝])[tail✝.reverse.length]? = (head✝ :: tail✝).head?
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ (tl.reverse ++ [hd])[tl.length]? = some hd

Tactic:
← List.length_reverse,

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ (tl.reverse ++ [hd])[tl.reverse.length]? = some hd