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

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

pp: case f00
⊢ ldiff 0 0 = 0

pp: case f0n
n✝ : PosNum
⊢ ldiff 0 (pos n✝) = bif false && !true then pos n✝ else 0

pp: case fn0
n✝ : PosNum
⊢ (pos n✝).ldiff 0 = bif true && !false then pos n✝ else 0

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

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

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)

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

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

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

case f00
⊢ ldiff 0 0 = 0

case f0n
n✝ : PosNum
⊢ ldiff 0 (pos n✝) = bif false && !true then pos n✝ else 0

case fn0
n✝ : PosNum
⊢ (pos n✝).ldiff 0 = bif true && !false then pos n✝ else 0

case fnn
m✝ n✝ : PosNum
⊢ (pos m✝).ldiff (pos n✝) = m✝.ldiff n✝

case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0

case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit b✝ n✝) = bit (true && !b✝) (bif false && !true then pos n✝ else 0)

case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff 1 = bit (a✝ && !true) (bif true && !false then pos m✝ else 0)

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

pp: case f00
⊢ ldiff 0 0 = 0

pp: case f0n
n✝ : PosNum
⊢ ldiff 0 (pos n✝) = bif false && !true then pos n✝ else 0

pp: case fn0
n✝ : PosNum
⊢ (pos n✝).ldiff 0 = bif true && !false then pos n✝ else 0

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

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

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

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

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

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

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

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

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

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

Tactic:
<;>

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

case f00
⊢ ldiff 0 0 = 0

case f0n
n✝ : PosNum
⊢ ldiff 0 (pos n✝) = bif false && !true then pos n✝ else 0

case fn0
n✝ : PosNum
⊢ (pos n✝).ldiff 0 = bif true && !false then pos n✝ else 0

case fnn
m✝ n✝ : PosNum
⊢ (pos m✝).ldiff (pos n✝) = m✝.ldiff n✝

case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0

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

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

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

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

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

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

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

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit true n✝) = bit (true && !true) (m✝.ldiff n✝)
Module: Mathlib.Data.Num.Lemmas

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

pp: case f00
⊢ 0 ^^^ 0 = 0

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

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

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

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

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)

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

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

Goal state after:
case gff
⊢ (false != false) = false

case f00
⊢ 0 ^^^ 0 = 0

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

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

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

case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0

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

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

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

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

pp: case f00
⊢ 0 ^^^ 0 = 0

pp: case f0n
n✝ : PosNum
⊢ 0 ^^^ pos n✝ = bif false != true then pos n✝ else 0

pp: case fn0
n✝ : PosNum
⊢ pos n✝ ^^^ 0 = bif true != false then pos n✝ else 0

pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝

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

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)

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

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

Goal state after:
case gff
⊢ (false != false) = false

case f00
⊢ 0 ^^^ 0 = 0

case f0n
n✝ : PosNum
⊢ 0 ^^^ pos n✝ = bif false != true then pos n✝ else 0

case fn0
n✝ : PosNum
⊢ pos n✝ ^^^ 0 = bif true != false then pos n✝ else 0

case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝

case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0

case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit b✝ n✝) = bit (true != b✝) (bif false != true then pos n✝ else 0)

case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).lxor 1 = bit (a✝ != true) (bif true != false then pos m✝ else 0)

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.StackTuringMachine

Goal state before:
pp: case pos
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))
i : ℕ
h : i = (S k).length
⊢ update (L.nth i) k (some (f v)) k = (ListBlank.mk (List.map some (update S k (f v :: S k) k)).reverse).nth i

pp: case neg
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))
i : ℕ
h : ¬i = (S k).length
⊢ L.nth i k = (ListBlank.mk (List.map some (update S k (f v :: S k) k)).reverse).nth i

Tactic:
<;>

Goal state after:
case pos
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))
i : ℕ
h : i = (S k).length
⊢ update (L.nth i) k (some (f v)) k = (ListBlank.mk (List.map some (update S k (f v :: S k) k)).reverse).nth i

case neg
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))
i : ℕ
h : ¬i = (S k).length
⊢ L.nth i k = (ListBlank.mk (List.map some (update S k (f v :: S k) k)).reverse).nth i
Module: Mathlib.Data.Num.Lemmas

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

pp: case f00
⊢ 0 ^^^ 0 = 0

pp: case f0n
n✝ : PosNum
⊢ 0 ^^^ pos n✝ = bif false != true then pos n✝ else 0

pp: case fn0
n✝ : PosNum
⊢ pos n✝ ^^^ 0 = bif true != false then pos n✝ else 0

pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝

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

pp: case p1b.false
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit false n✝) = bit (true != false) (bif false != true then pos n✝ else 0)

pp: case p1b.true
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit true n✝) = bit (true != true) (bif false != true then pos n✝ else 0)

pp: case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).lxor 1 = bit (false != true) (bif true != false then pos m✝ else 0)

pp: case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).lxor 1 = bit (true != true) (bif true != false then pos m✝ else 0)

pp: case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit false n✝) = bit (false != false) (m✝.lxor n✝)

pp: case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit true n✝) = bit (false != true) (m✝.lxor n✝)

pp: case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit false n✝) = bit (true != false) (m✝.lxor n✝)

pp: case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit true n✝) = bit (true != true) (m✝.lxor n✝)

Tactic:
<;>

Goal state after:
case gff
⊢ (false != false) = false

case f00
⊢ 0 ^^^ 0 = 0

case f0n
n✝ : PosNum
⊢ 0 ^^^ pos n✝ = bif false != true then pos n✝ else 0

case fn0
n✝ : PosNum
⊢ pos n✝ ^^^ 0 = bif true != false then pos n✝ else 0

case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝

case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0

case p1b.false
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit false n✝) = bit (true != false) (bif false != true then pos n✝ else 0)

case p1b.true
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit true n✝) = bit (true != true) (bif false != true then pos n✝ else 0)

case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).lxor 1 = bit (false != true) (bif true != false then pos m✝ else 0)

case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).lxor 1 = bit (true != true) (bif true != false then pos m✝ else 0)

case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit false n✝) = bit (false != false) (m✝.lxor n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit true n✝) = bit (false != true) (m✝.lxor n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit false n✝) = bit (true != false) (m✝.lxor n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit true n✝) = bit (true != true) (m✝.lxor n✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : ℕ
⊢ ↑(zero <<< n) = ↑zero <<< n

pp: case pos
n : ℕ
a✝ : PosNum
⊢ ↑(pos a✝ <<< n) = ↑(pos a✝) <<< n

Tactic:
<;>

Goal state after:
case zero
n : ℕ
⊢ ↑(zero <<< n) = ↑zero <<< n

case pos
n : ℕ
a✝ : PosNum
⊢ ↑(pos a✝ <<< n) = ↑(pos a✝) <<< n
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move.left
Γ : 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
q : Stmt Γ Λ σ
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.move Dir.left q)
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.left q))

pp: case move.right
Γ : 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
q : Stmt Γ Λ σ
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.move Dir.right q)
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.right q))

Tactic:
<;>

Goal state after:
case move.left
Γ : 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
q : Stmt Γ Λ σ
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.move Dir.left q)
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.left q))

case move.right
Γ : 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
q : Stmt Γ Λ σ
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.move Dir.right q)
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.right q))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : ℕ
⊢ ↑(zero >>> n) = ↑zero >>> n

pp: case pos
n : ℕ
m : PosNum
⊢ ↑(pos m >>> n) = ↑(pos m) >>> n

Tactic:
<;>

Goal state after:
case zero
n : ℕ
⊢ ↑(zero >>> n) = ↑zero >>> n

case pos
n : ℕ
m : PosNum
⊢ ↑(pos m >>> n) = ↑(pos m) >>> n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.one
⊢ ↑(one >>> 0) = ↑(pos one) >>> 0

pp: case pos.zero.bit1
a✝ : PosNum
⊢ ↑(a✝.bit1 >>> 0) = ↑(pos a✝.bit1) >>> 0

pp: case pos.zero.bit0
a✝ : PosNum
⊢ ↑(a✝.bit0 >>> 0) = ↑(pos a✝.bit0) >>> 0

Tactic:
<;>

Goal state after:
case pos.zero.one
⊢ ↑(one >>> 0) = ↑(pos one) >>> 0

case pos.zero.bit1
a✝ : PosNum
⊢ ↑(a✝.bit1 >>> 0) = ↑(pos a✝.bit1) >>> 0

case pos.zero.bit0
a✝ : PosNum
⊢ ↑(a✝.bit0 >>> 0) = ↑(pos a✝.bit0) >>> 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(one >>> (n + 1)) = ↑(pos one) >>> (n + 1)

pp: case pos.succ.bit1
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.bit1 >>> (n + 1)) = ↑(pos m.bit1) >>> (n + 1)

pp: case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.bit0 >>> (n + 1)) = ↑(pos m.bit0) >>> (n + 1)

Tactic:
<;>

Goal state after:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(one >>> (n + 1)) = ↑(pos one) >>> (n + 1)

case pos.succ.bit1
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.bit1 >>> (n + 1)) = ↑(pos m.bit1) >>> (n + 1)

case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.bit0 >>> (n + 1)) = ↑(pos m.bit0) >>> (n + 1)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero
m : PosNum
⊢ m.testBit 0 = (↑m).testBit 0

pp: case pos.succ
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit (n✝ + 1) = (↑m).testBit (n✝ + 1)

Tactic:
<;>

Goal state after:
case pos.zero
m : PosNum
⊢ m.testBit 0 = (↑m).testBit 0

case pos.succ
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit (n✝ + 1) = (↑m).testBit (n✝ + 1)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.one
⊢ one.testBit 0 = (↑one).testBit 0

pp: case pos.zero.bit1
m : PosNum
⊢ m.bit1.testBit 0 = (↑m.bit1).testBit 0

pp: case pos.zero.bit0
m : PosNum
⊢ m.bit0.testBit 0 = (↑m.bit0).testBit 0

pp: case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ one.testBit (n✝ + 1) = (↑one).testBit (n✝ + 1)

pp: case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.bit1.testBit (n✝ + 1) = (↑m.bit1).testBit (n✝ + 1)

pp: case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.bit0.testBit (n✝ + 1) = (↑m.bit0).testBit (n✝ + 1)

Tactic:
<;>

Goal state after:
case pos.zero.one
⊢ one.testBit 0 = (↑one).testBit 0

case pos.zero.bit1
m : PosNum
⊢ m.bit1.testBit 0 = (↑m.bit1).testBit 0

case pos.zero.bit0
m : PosNum
⊢ m.bit0.testBit 0 = (↑m.bit0).testBit 0

case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ one.testBit (n✝ + 1) = (↑one).testBit (n✝ + 1)

case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.bit1.testBit (n✝ + 1) = (↑m.bit1).testBit (n✝ + 1)

case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.bit0.testBit (n✝ + 1) = (↑m.bit0).testBit (n✝ + 1)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case goto
Γ : 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
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l))

Tactic:
refine supportsStmt_read _ fun a _ s ↦ ?_

Goal state after:
case goto
Γ : 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
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
a : Γ
x✝ : Bool
s : σ
⊢ (fun x s ↦ Λ'.normal (l a s)) x✝ s ∈ trSupp M S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
a✝ : Dir
⊢ TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.move a✝) q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match TM0.Stmt.move a✝ with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

pp: case write
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
a✝ : Γ
⊢ TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.write a✝) q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match TM0.Stmt.write a✝ with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
<;>

Goal state after:
case move
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
a✝ : Dir
⊢ TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.move a✝) q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match TM0.Stmt.move a✝ with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

case write
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
a✝ : Γ
⊢ TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.write a✝) q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match TM0.Stmt.write a✝ with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }