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

Goal state before:
pp: case nil
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
f : List.Vector Bool [].length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux [].length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux (f ⟨[], ⋯⟩) v (Tape.mk' (ListBlank.append ([].reverseAux l₁) L') R')

Tactic:
rfl

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

Goal state before:
pp: case e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
x✝ : (k : K) → Option (Γ k)
⊢ { f := Prod.mk false, map_pt' := ⋯ }.f (f x✝) =
    (({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).2)

Tactic:
rfl

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

Goal state before:
pp: case false
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (false :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ (bif false then
      stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))) =
    stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

Tactic:
rfl

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

Goal state before:
pp: case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ TM2.SupportsStmt S (stRun (push a✝) q) ↔ TM2.SupportsStmt S q

Tactic:
rfl

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

Goal state before:
pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ TM2.SupportsStmt S (stRun (peek a✝) q) ↔ TM2.SupportsStmt S q

Tactic:
rfl

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

Goal state before:
pp: case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ TM2.SupportsStmt S (stRun (pop a✝) q) ↔ TM2.SupportsStmt S q

Tactic:
rfl

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

Goal state before:
pp: case true
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (true :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ (bif true then
      stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))) =
    stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

Tactic:
rfl

Goal state after:
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 : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) S

Tactic:
rfl

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

Goal state before:
pp: case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ trNormal (stRun (StAct.push a✝) q) = goto fun x x_1 ↦ go k (StAct.push a✝) q

Tactic:
rfl

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

Goal state before:
pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trNormal (stRun (StAct.peek a✝) q) = goto fun x x_1 ↦ go k (StAct.peek a✝) q

Tactic:
rfl

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

Goal state before:
pp: case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trNormal (stRun (StAct.pop a✝) q) = goto fun x x_1 ↦ go k (StAct.pop a✝) q

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mpr.cons.cons.cons.refine_2
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ P.star.rmatch U.flatten = true

Tactic:
grind

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (f (a ::ᵥ ⟨l₂, ⋯⟩)) v (Tape.mk' (ListBlank.append (l₂.reverseAux (a :: l₁)) L') R') =
    stepAux (f ⟨a :: l₂, ⋯⟩) v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case char
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
x : List α
⊢ x = [a✝] ↔ x ∈ (char a✝).matches'

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

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

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

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

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

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

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

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

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

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case plus
α : Type u_1
inst✝ : DecidableEq α
a✝¹ a✝ : RegularExpression α
ih₁ : ∀ (x : List α), a✝¹.rmatch x = true ↔ x ∈ a✝¹.matches'
ih₂ : ∀ (x : List α), a✝.rmatch x = true ↔ x ∈ a✝.matches'
x : List α
⊢ x ∈ a✝¹.matches' ∨ x ∈ a✝.matches' ↔ x ∈ (a✝¹ + a✝).matches'

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ (match P ^ 0 with
    | zero => 0
    | epsilon => 1
    | char a => char (f a)
    | R.plus S => map f R + map f S
    | R.comp S => map f R * map f S
    | R.star => (map f R).star) =
    (match P with
      | zero => 0
      | epsilon => 1
      | char a => char (f a)
      | R.plus S => map f R + map f S
      | R.comp S => map f R * map f S
      | R.star => (map f R).star) ^
      0

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
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:
rfl

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:
rfl

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

Goal state before:
pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit false n✝) = bit (false && false) (m✝.land n✝)

Tactic:
rfl

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

Goal state before:
pp: case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit true n✝) = bit (false && true) (m✝.land n✝)

Tactic:
rfl

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

Goal state before:
pp: case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit false n✝) = bit (true && false) (m✝.land n✝)

Tactic:
rfl

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

Goal state before:
pp: case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit true n✝) = bit (true && true) (m✝.land n✝)

Tactic:
rfl

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

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : List.Vector ℕ m), cg.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval ↑v = pure <$> f v
v : List.Vector ℕ m
⊢ (do
      let a ← Vector.mOfFn fun i ↦ g i v
      pure <$> f a) =
    do
    let a ← Vector.mOfFn fun i ↦ g i v
    pure <$> f a

Tactic:
rfl

Goal state after:
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right)^[(S k).length]
          (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a ↦ update a k (some (f v))) (S k).length L))))) =
    TM1.stepAux q v ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[(S k).length]) (Tape.mk' ∅ (addBottom ?m.135)))

Tactic:
rfl

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

Goal state before:
pp: m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
v : List.Vector ℕ m
⊢ Part.some [] = Subtype.val <$> Part.some Vector.nil

Tactic:
rfl

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

Goal state before:
pp: m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval ↑v = pure <$> g 0 v
cl : Code
hl : ∀ (v : List.Vector ℕ m), cl.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i.succ v
v : List.Vector ℕ m
⊢ (do
      let a ← g 0 v
      let a_1 ← Vector.mOfFn fun i ↦ g i.succ v
      Part.some (a :: ↑a_1)) =
    do
    let a ← g 0 v
    let a_1 ← Vector.mOfFn fun i ↦ g i.succ v
    Subtype.val <$> Part.some (a ::ᵥ a_1)

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff (PosNum.bit false n✝) = bit (false && !false) (m✝.ldiff n✝)

Tactic:
rfl

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

Goal state before:
pp: case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff (PosNum.bit true n✝) = bit (false && !true) (m✝.ldiff n✝)

Tactic:
rfl

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

Goal state before:
pp: case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit false n✝) = bit (true && !false) (m✝.ldiff n✝)

Tactic:
rfl

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

Goal state before:
pp: case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit true n✝) = bit (true && !true) (m✝.ldiff n✝)

Tactic:
rfl

Goal state after:
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))
    (bif p R.head v then stepAux (trNormal dec q₁) v (trTape' enc0 L R)
    else stepAux (trNormal dec q₂) v (trTape' enc0 L R))
    (trCfg enc enc0 (bif p R.head v then stepAux q₁ v (Tape.mk' L R) else stepAux q₂ v (Tape.mk' L R)))

Tactic:
grind

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

Goal state before:
pp: n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i : Fin n✝
n : ℕ
x✝ : List.Vector ℕ n.succ
a : ℕ
as : List ℕ
property✝ : (a :: as).length = n.succ
⊢ Part.some [a] = pure <$> Part.some (List.Vector.head ⟨a :: as, property✝⟩)

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after: