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

Goal state before:
pp: x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
⊢ ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode c) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode c))))
          (k', c') n =
        evaln k' c' n

Tactic:
intro k₁

Goal state after:
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
k₁ : ℕ
⊢ ∀ {c' : Code} {n : ℕ},
    Nat.pair k₁ (encode c') < Nat.pair k (encode c) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode c))))
          (k₁, c') n =
        evaln k₁ c' n
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
⊢ (fun x_1 ↦ x ++ x_1) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.evalFrom S x)

Tactic:
ext y

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x y : List α
⊢ y ∈ (fun x_1 ↦ x ++ x_1) ⁻¹' M.acceptsFrom S ↔ y ∈ M.acceptsFrom (M.evalFrom S x)
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case base
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
s✝ : σ
a✝ : s✝ ∈ {t}
⊢ s✝ ∈ M.εClosure S

Tactic:
subst_vars

Goal state after:
case base
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s✝ : σ
left✝ : s✝ ∈ S
⊢ s✝ ∈ M.εClosure S
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case step
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {t} s✝
a_ih✝ : s✝ ∈ M.εClosure S
⊢ t✝ ∈ M.εClosure S

Tactic:
subst_vars

Goal state after:
case step
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {t} s✝
a_ih✝ : s✝ ∈ M.εClosure S
⊢ t✝ ∈ M.εClosure S
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a + b + c = a + (b + c)

Tactic:
(Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a + b = b + a

Tactic:
(Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a * b * c = a * (b * c)

Tactic:
(Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), 1 * a = a

Tactic:
(Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), a * 1 = a

Tactic:
(Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a * b = b * a

Tactic:
(Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), a ≤ a

Tactic:
(Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ M.accepts.leftQuotient x = M.acceptsFrom (M.eval x)

Tactic:
ext y

Goal state after:
α : Type u
σ : Type v
M : DFA α σ
x y : List α
⊢ y ∈ M.accepts.leftQuotient x ↔ y ∈ M.acceptsFrom (M.eval x)
Module: Mathlib.Computability.RE

Goal state before:
pp: f₁ f₂ : ℕ → ℕ
hf₁ : Computable f₁
hf₂ : Computable f₂
c : ℕ → Prop
inst✝ : DecidablePred c
hc : ComputablePred c
⊢ Computable fun k ↦ if c k then f₁ k else f₂ k

Tactic:
simpa [Bool.cond_decide] using hc.decide.cond hf₁ hf₂

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

Goal state before:
pp: case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝ : Dir
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = move a✝ q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h)

Goal state after:
case move.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
a✝ : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S q
IH : move a✝ q ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S (move a✝ q)
⊢ SupportsStmt S (move a✝ q)

case move.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝ : Dir
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
rcases h with (rfl | h)

Goal state after:
case write.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S q
IH : write a✝ q ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S (write a✝ q)
⊢ SupportsStmt S (write a✝ q)

case write.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
rcases h with (rfl | h)

Goal state after:
case load.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
hs : SupportsStmt S q
IH : load a✝ q ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S (load a✝ q)
⊢ SupportsStmt S (load a✝ q)

case load.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux (i + 1) f)

Tactic:
constructor <;> apply IH

Goal state after:
case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ ∀ (v : List.Vector Bool i), SupportsStmt S (f (true ::ᵥ v))

case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ ∀ (v : List.Vector Bool i), SupportsStmt S (f (false ::ᵥ v))
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case load
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝¹ : σ → σ
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ = load a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h)

Goal state after:
case load.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
a✝¹ : σ → σ
a✝ : Stmt Γ Λ σ
hs : SupportsStmt S a✝
IH : load a✝¹ a✝ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S (load a✝¹ a✝)
⊢ SupportsStmt S (load a✝¹ a✝)

case load.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝¹ : σ → σ
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁
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 Λ
q₁ : Stmt Γ Λ σ
k✝ : K
a✝¹ : σ → Γ k✝
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ = push k✝ a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h)

Goal state after:
case push.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k✝ : K
a✝¹ : σ → Γ k✝
a✝ : Stmt Γ Λ σ
hs : SupportsStmt S a✝
IH : push k✝ a✝¹ a✝ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S (push k✝ a✝¹ a✝)
⊢ SupportsStmt S (push k✝ a✝¹ a✝)

case push.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
k✝ : K
a✝¹ : σ → Γ k✝
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁
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 Λ
q₁ : Stmt Γ Λ σ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ = peek k✝ a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h)

Goal state after:
case peek.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
hs : SupportsStmt S a✝
IH : peek k✝ a✝¹ a✝ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S (peek k✝ a✝¹ a✝)
⊢ SupportsStmt S (peek k✝ a✝¹ a✝)

case peek.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁
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 Λ
q₁ : Stmt Γ Λ σ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ = pop k✝ a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h)

Goal state after:
case pop.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
hs : SupportsStmt S a✝
IH : pop k✝ a✝¹ a✝ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S (pop k✝ a✝¹ a✝)
⊢ SupportsStmt S (pop k✝ a✝¹ a✝)

case pop.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁
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)) (update S k (stWrite v (S k) (StAct.peek f)))

Tactic:
unfold stWrite; rw [Function.update_eq_self]; rfl

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

Goal state before:
pp: v : List ℕ
⊢ pred.eval v = pure [v.headI.pred]

Tactic:
simp [pred]; cases v.headI <;> simp

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

Tactic:
subst k'
      split_ifs with h
        <;> simp only [List.reverse_cons, Function.update_self, ListBlank.nth_mk, List.map]
      · rw [List.getI_eq_getElem _, List.getElem_append_right] <;>
        simp only [List.length_append, List.length_reverse, List.length_map, ← h,
          Nat.sub_self, List.length_singleton, List.getElem_singleton,
          le_refl, Nat.lt_succ_self]
      rw [← proj_map_nth, hL, ListBlank.nth_mk]
      rcases lt_or_gt_of_ne h with h | h
      · rw [List.getI_append]
        simpa only [List.length_map, List.length_reverse] using h
      · rw [List.getI_eq_default, List.getI_eq_default] <;>
          simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
            List.length_append, List.length_map]

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

Goal state before:
pp: case pop.nil
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) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k [].tail k_1)).reverse) ∧
      (bif ((Tape.move Dir.right)^[[].length] (Tape.mk' ∅ (addBottom L))).head.1 then
          TM1.stepAux q (f v none) ((Tape.move Dir.right)^[[].length] (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[[].length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right)^[[].length] (Tape.mk' ∅ (addBottom L)))).head.1,
                update (Tape.move Dir.left ((Tape.move Dir.right)^[[].length] (Tape.mk' ∅ (addBottom L)))).head.2 k
                  none)
              (Tape.move Dir.left ((Tape.move Dir.right)^[[].length] (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (f v [].head?) ((Tape.move Dir.right)^[[].tail.length] (Tape.mk' ∅ (addBottom L')))

Tactic:
simp only [Tape.mk'_head, ListBlank.head_cons, Tape.move_left_mk', List.length,
        List.head?, iterate_zero_apply, List.tail_nil]

Goal state after:
case pop.nil
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) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k [] k_1)).reverse) ∧
      (bif (addBottom L).head.1 then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
        else
          TM1.stepAux q (f v (∅.head.2 k))
            (Tape.write (∅.head.1, update ∅.head.2 k none) (Tape.mk' ∅.tail (ListBlank.cons ∅.head (addBottom L))))) =
        TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L'))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case zero'
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k (0 :: v)) k v) = do
    let v ← Code.zero'.eval v
    eval step (Cfg.ret k v)

Tactic:
simp only [Code.eval, pure_bind]

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

Goal state before:
pp: case succ
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k [v.headI.succ]) k v) = do
    let v ← Code.succ.eval v
    eval step (Cfg.ret k v)

Tactic:
simp only [Code.eval, pure_bind]

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

Goal state before:
pp: case tail
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k v.tail) k v) = do
    let v ← Code.tail.eval v
    eval step (Cfg.ret k v)

Tactic:
simp only [Code.eval, pure_bind]

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X Y : CompHaus
Z : Stonean
e : Z.compHaus ⟶ Y
f : X ⟶ Y
inst✝ : Epi f
⊢ lift e f ≫ f = e

Tactic:
simp [lift]

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X Y : Profinite
Z : Stonean
e : Stonean.toProfinite.obj Z ⟶ Y
f : X ⟶ Y
inst✝ : Epi f
⊢ lift e f ≫ f = e

Tactic:
simp [lift]

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : LocallyConnectedSpace X
x : X
⊢ ofPred ((connectedComponentSetoid X) x) = connectedComponent x

Tactic:
ext y

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : LocallyConnectedSpace X
x y : X
⊢ y ∈ ofPred ((connectedComponentSetoid X) x) ↔ y ∈ connectedComponent x
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
⊢ ∃ I, W = I.sup fun i ↦ i.1 ×ˢ i.2

Tactic:
rcases W.2.1.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦
    (U x ×ˢ V x).2.isOpen.mem_nhds ⟨hxU x hx, hxV x hx⟩) with ⟨I, hIW, hWI⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
⊢ ∃ I, W = I.sup fun i ↦ i.1 ×ˢ i.2
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case h.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
x : X × Y
hx : x ∈ W
⊢ x ∈ I.sup ((fun i ↦ i.1 ×ˢ i.2) ∘ fun x ↦ (U x, V x))

Tactic:
rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩

Goal state after:
case h.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
x : X × Y
hx : x ∈ W
i : X × Y
hi : i ∈ I
hxi : x ∈ ↑(U i) ×ˢ ↑(V i)
⊢ x ∈ I.sup ((fun i ↦ i.1 ×ˢ i.2) ∘ fun x ↦ (U x, V x))
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case empty
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
S : Set (Set ↑(F.obj j))
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ ∅, P e ∈ S) → ⋂ e ∈ ∅, P e ∈ S

Tactic:
intro P he _hh
          simpa

Goal state after:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V

Tactic:
obtain ⟨j0, hj0⟩ := IsCofiltered.inf_objs_exists (G.image j)

Goal state after:
case refine_3
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push
q' : Λ'
k✝ : K'
s✝ : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.push k✝ s✝ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k✝ s✝ q)

Tactic:
| push _ _ q q_ih =>

Goal state after:
case push
q' : Λ'
k✝ : K'
s✝ : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.push k✝ s✝ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k✝ s✝ q)