mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ 2 ∣ 4

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: α : Type u_1
Γ : Type u_2
e : Encoding α Γ
⊢ Function.Injective e.encode

Tactic:
by
  refine fun _ _ h => Option.some_injective _ ?_
  rw [← e.decode_encode, ← e.decode_encode, h]

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: α : Type u_1
β : Type u_2
Γ₁ : Type u_3
Γ₂ : Type u_4
ea : Encoding α Γ₁
eb : Encoding β Γ₂
x : α × β
⊢ Option.map₂ Prod.mk
      (ea.decode (List.filterMap Sum.getLeft? (List.map Sum.inl (ea.encode x.1) ++ List.map Sum.inr (eb.encode x.2))))
      (eb.decode
        (List.filterMap Sum.getRight? (List.map Sum.inl (ea.encode x.1) ++ List.map Sum.inr (eb.encode x.2)))) =
    some x

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
⊢ M.evalFrom (S ∪ T) [] = M.evalFrom S [] ∪ M.evalFrom T []

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
⊢ M.evalFrom (⋃ i, s i) [] = ⋃ i, M.evalFrom (s i) []

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
κ : ι → Sort u_2
f : (i : ι) → κ i → Set σ
x : List α
⊢ M.evalFrom (⋃ i, ⋃ j, f i j) x = ⋃ i, ⋃ j, M.evalFrom (f i j) x

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
x : List α
⊢ s ∈ ⋃ s ∈ S, M.evalFrom {s} x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
κ : ι → Sort u_2
f : (i : ι) → κ i → Set σ
⊢ M.acceptsFrom (⋃ i, ⋃ j, f i j) = ⋃ i, ⋃ j, M.acceptsFrom (f i j)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case nil
α : Type u_1
⊢ (¬∀ (x : Option α), x ∈ [] → x.isSome = true) ↔ none ∈ []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : Option α
⊢ (l.concat x).reduceOption = l.reduceOption ++ x.toList

Tactic:
induction l generalizing x with

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s✝ t : σ
x : List α
p : Nonempty (M.Path s✝ t x)
s : σ
⊢ s ∈ M.evalFrom {s} []

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ M.IsPath s t [] ↔ s = t

Tactic:
by
  rw [isPath_iff]
  simp [eq_comm]

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

Goal state before:
pp: m n : Num
x✝ : ↑m ∣ ↑n
k : ℕ
e : ↑n = ↑m * k
⊢ ↑(↑m * k) = m * ↑k

Tactic:
simp

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

Goal state before:
pp: m n : PosNum
h : ↑m = ↑n
⊢ pos m = pos n

Tactic:
by rw [← PosNum.of_to_nat, ← PosNum.of_to_nat, h]

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

Goal state before:
pp: n : PosNum
⊢ (↑n).size + 1 = (↑n.bit1).size

Tactic:
cast_bit1,

Goal state after:
n : PosNum
⊢ (↑n).size + 1 = (↑n + ↑n + 1).size
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: case nil
α : Type u
L : Language α
⊢ ↑(L.toDFA.eval []) = L.leftQuotient []

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
h : (Set.range L.leftQuotient).Finite
⊢ L.toDFA.accepts = L

Tactic:
simp

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

Goal state before:
pp: ⊢ ofNat' 0 = ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
⊢ (mOfFn fun i ↦ (↑fun v ↦ v.get i.succ) v) >>= f = f (ofFn fun x ↦ v.get x.succ)

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n m : ℕ
f : List.Vector ℕ m →. ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Partrec' f
hg : Vec g
v : List.Vector ℕ n
⊢ (mOfFn fun i ↦ ↑(some ((g v).get i))) >>= f = f (g v)

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: 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 : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
y : ℕ
⊢ y ∈ (Option.some y <|> Code.evaln k cg n)

Tactic:
simp

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

Tactic:
simp

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
Module: Mathlib.Computability.PartrecBasis

Goal state before:
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:
simp

Goal state after:
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.Data.Num.Lemmas

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
x✝ : ℝ
⊢ f x✝ = (g + (f - g)) x✝

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
⊢ l = l ++ List.replicate 0 default

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l₁ : List Γ
i j : ℕ
⊢ l₁ ++ List.replicate i default ++ List.replicate j default = l₁ ++ List.replicate (i + j) default

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
⊢ Reaches f a b ∧ f b = none

Tactic:
rcases e : f a with - | a'

Goal state after:
case refine_1.none
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a b ∧ f b = none

case refine_1.some
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
⊢ Reaches f a b ∧ f b = none
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
⊢ (bif Sum.casesOn (f a) (fun b ↦ true) fun b ↦ false then
      Sum.casesOn (f a) (fun b ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun c ↦ Part.some Option.none
    else Sum.casesOn (f a) (fun b ↦ Part.some Option.none) fun b ↦ Part.map Option.some (h (a, b).1 (a, b).2)) =
    Part.map Option.some (Sum.casesOn (f a) (g a) (h a))

Tactic:
by cases f a <;> simp only [Bool.cond_true, Bool.cond_false]

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p : α → Prop
w✝ : DecidablePred p
hp : Computable fun a ↦ decide (p a)
⊢ ∀ (n : α), (!decide (p n)) = decide ¬p n

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: case unit.false
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a ↦ f a = true
n : α
⊢ (PUnit.unit ∈ bif false then Part.some () else Part.none) ↔
    PUnit.unit ∈ Part.assert (false = true) fun x ↦ Part.some ()

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: case unit.true
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a ↦ f a = true
n : α
⊢ (PUnit.unit ∈ bif true then Part.some () else Part.none) ↔ PUnit.unit ∈ Part.assert (true = true) fun x ↦ Part.some ()

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
⊢ ∀ (x : σ₂), tr g₁ x → Reaches₁ f₂ b✝ x → ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
intro g₂ gg cg
        rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩
        cases Option.mem_unique cd cd'
        exact ⟨_, _, dg, gg, ae.tail eg⟩

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
d₁ : σ₁
hfc : f₁ c₁ = some d₁
d₂ : σ₂
left✝ : tr d₁ d₂
bd : Reaches₁ f₂ b₂ d₂
⊢ some d₁ = none

Tactic:
rcases TransGen.head'_iff.1 bd with ⟨e, h, _⟩

Goal state after:
case refl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
d₁ : σ₁
hfc : f₁ c₁ = some d₁
d₂ : σ₂
left✝ : tr d₁ d₂
bd : Reaches₁ f₂ b₂ d₂
e : σ₂
h : e ∈ f₂ b₂
right✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) e d₂
⊢ some d₁ = none
Module: Mathlib.Computability.TuringMachine.Tape

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

Tactic:
simp

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

Goal state before:
pp: case some.write
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T }.q ∈ S
q' : Λ
a : Γ
⊢ Option.map (fun x ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun x ↦
          { q := x.1,
            Tape :=
              match x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        (some (q', Stmt.write a))) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) (some (q', Stmt.write a)))

Tactic:
· simp only [Option.map_some, Tape.map_write]
      rfl

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p : α → Prop
⊢ ∀ (a : α), p a ↔ p (id a)

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
x✝ : β
⊢ q x✝ = ((q ∘ ⇑e) ∘ ⇑e.symm) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ { r := ManyOneEquiv, iseqv := _proof_1 } (toNat p) (toNat q) ↔ ManyOneEquiv p q

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: case h
p✝ : Set ℕ
⊢ of p✝ ≤ of p✝

Tactic:
simp

Goal state after:
case h
p✝ : Set ℕ
⊢ p✝ ≤₀ p✝
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝ : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ some q ∈ stmts M S → SupportsStmt S q

Tactic:
by
  simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]
  exact fun l ls h ↦ stmts₁_supportsStmt_mono h (ss.2 _ ls)

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

Goal state before:
pp: case right.some.none
Γ : 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 : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
h₁ : ((none, v'), s) ∈ tr M (some q, v) a
⊢ none ∈ TM1.stmts M S

pp: case right.some.some
Γ : 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 : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : ((some val✝, v'), s) ∈ tr M (some q, v) a
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
· exact Multiset.mem_cons_self _ _

Goal state after:
case right.some.some
Γ : 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 : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : ((some val✝, v'), s) ∈ tr M (some q, v) a
⊢ some val✝ ∈ TM1.stmts M S
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ some q ∈ stmts M S → SupportsStmt S q

Tactic:
by
  simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]
  exact fun l ls h ↦ stmts₁_supportsStmt_mono h (ss.2 _ ls)

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
l : List ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.mk l)) =
    ListBlank.mk l

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : 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
⊢ b :: t ∈ (b :: t) :: U

Tactic:
simp

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

Goal state before:
pp: case zero
v : List ℕ
⊢ Nat.rec (Part.some [0]) (fun y x ↦ Part.some [y]) 0 = Part.some [0 - 1]

Tactic:
simp

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

Goal state before:
pp: case succ
v : List ℕ
n✝ : ℕ
⊢ Nat.rec (Part.some [0]) (fun y x ↦ Part.some [y]) (n✝ + 1) = Part.some [n✝ + 1 - 1]

Tactic:
simp

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

Goal state before:
pp: case zero
m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ 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

Tactic:
exact ⟨nil, fun v => by simp [Vector.mOfFn]; rfl⟩

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

Goal state before:
pp: case prim.succ
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
⊢ ∃ c, ∀ (v : List.Vector ℕ 1), c.eval ↑v = pure <$> (↑fun v ↦ v.head.succ) v

Tactic:
exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩

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
⊢ head.eval ↑⟨a :: as, property✝⟩ = pure <$> (↑fun v ↦ v.get 0) ⟨a :: as, property✝⟩

Tactic:
simp

Goal state after:
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✝⟩)
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 → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
q : Stmt Γ Λ σ
hs : 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')

Tactic:
hw

Goal state after:
Γ : 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 Γ Λ σ
hs : SupportsStmt S q
hw : ∀ 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')
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
obtain - | m | m := m

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.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(pos one) < 2 ^ (n + 1)

Tactic:
simp

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

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

Tactic:
obtain - | m | m := m

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

Goal state before:
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:
obtain - | m | m := m

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