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

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

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))
k' : K
i : ℕ
h' : ¬k' = k
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))
k' : K
i : ℕ
h' : ¬k' = k
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.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
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

Tactic:
Function.update_of_ne h',

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))
k' : K
i : ℕ
h' : ¬k' = k
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.Computability.TuringMachine.StackTuringMachine

Goal state before:
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))
k' : K
i : ℕ
h' : ¬k' = k
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:
Function.update_of_ne h',

Goal state after:
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))
k' : K
i : ℕ
h' : ¬k' = k
h✝ : ¬i = (S k).length
⊢ L.nth i k' = (ListBlank.mk (List.map some (S k')).reverse).nth i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case rfind.mp
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
⊢ v' ∈
      PFun.fix
        (fun v ↦
          (cf.eval v).bind fun y ↦
            Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
        v₀ →
    ∀ (n_1 : ℕ),
      v₀ = n_1 :: ↑v →
        (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
          ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
h1

Goal state after:
case rfind.mp
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
h1 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      v₀
⊢ ∀ (n_1 : ℕ),
    v₀ = n_1 :: ↑v →
      (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
        ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
⊢ (if i = tl.length then update (L.nth i) k none else L.nth i) k' =
    (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i

Tactic:
split_ifs

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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h✝ : i = tl.length
⊢ update (L.nth i) k none k' = (ListBlank.mk (List.map some (update S k (hd :: tl).tail 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h✝ : ¬i = tl.length
⊢ L.nth i k' = (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i
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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h✝ : i = tl.length
⊢ update (L.nth i) k none k' = (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i

Tactic:
Function.update_of_ne h',

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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h✝ : i = tl.length
⊢ L.nth i k' = (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h✝ : ¬i = tl.length
⊢ L.nth i k' = (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i

Tactic:
Function.update_of_ne h',

Goal state after:
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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
h' : ¬k' = k
h✝ : ¬i = tl.length
⊢ L.nth i k' = (ListBlank.mk (List.map some (S k')).reverse).nth i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ (if v.headI = 0 then a✝.eval v.tail >>= k'.eval else a✝¹.fix.eval v.tail >>= (a✝.then k').eval) =
    (if v.headI = 0 then a✝.eval v.tail else a✝¹.fix.eval v.tail >>= a✝.eval) >>= k'.eval

Tactic:
split_ifs

Goal state after:
case pos
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
h✝ : v.headI = 0
⊢ a✝.eval v.tail >>= k'.eval = a✝.eval v.tail >>= k'.eval

case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
h✝ : ¬v.headI = 0
⊢ a✝¹.fix.eval v.tail >>= (a✝.then k').eval = a✝¹.fix.eval v.tail >>= a✝.eval >>= k'.eval
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ (if v.headI = 0 then (stepRet a✝ v.tail).then k' else stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail) =
    (if v.headI = 0 then stepRet a✝ v.tail else stepNormal a✝¹ (Cont.fix a✝¹ a✝) v.tail).then k'

Tactic:
split_ifs

Goal state after:
case pos
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : v.headI = 0
⊢ (stepRet a✝ v.tail).then k' = (stepRet a✝ v.tail).then k'

case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : ¬v.headI = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail = (stepNormal a✝¹ (Cont.fix a✝¹ a✝) v.tail).then k'
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
⊢ i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π

Tactic:
Iso.inv_comp_eq

Goal state after:
α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
⊢ Sigma.desc π = i.hom ≫ finiteCoproduct.desc X π
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case mp
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
let N := { s // IsClopen s ∧ x ∈ s }

Goal state after:
case mp
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s // IsClopen s ∧ x ∈ s }
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
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
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
l' : Λ' K Γ Λ σ
h : l' ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
suffices ∀ (q) (_ : TM2.SupportsStmt S q) (_ : ∀ x ∈ trStmts₁ q, x ∈ trSupp M S),
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
        ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l') by
      rcases Finset.mem_biUnion.1 h with ⟨l, lS, h⟩
      have :=
        this _ (ss.2 l lS) fun x hx ↦ Finset.mem_biUnion.2 ⟨_, lS, Finset.mem_insert_of_mem hx⟩
      rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ h]

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
l' : Λ' K Γ Λ σ
h : l' ∈ trSupp M S
⊢ ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt S q →
      (∀ x ∈ trStmts₁ q, x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧ ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.cons.false
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k₁ = a' :: Sk
e₂ : p a' = false
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Tactic:
simp only [e₂, cond] at e

Goal state after:
case cons.cons.false
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.cons.true
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k₁ = a' :: Sk
e₂ : p a' = true
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Tactic:
simp only [e₂, cond] at e

Goal state after:
case cons.cons.true
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = true
e : ([], some a', Sk) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

Tactic:
rw [stepRet, IH, bind_pure_comp]

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

Goal state before:
pp: case fix
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) =
    Cfg.halt <$> if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval

Tactic:
split_ifs

Goal state after:
case pos
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : v.headI = 0
⊢ eval step (stepRet k v.tail) = Cfg.halt <$> k.eval v.tail

case neg
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : ¬v.headI = 0
⊢ eval step (stepNormal f (Cont.fix f k) v.tail) = Cfg.halt <$> (f.fix.eval v.tail >>= k.eval)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos.refine_3
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ X ⁻¹' {a})

Tactic:
exact (C_sub c.mem).left.inter <| (T1Space.t1 a).preimage X_cont

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos.refine_4
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ X ⁻¹' {a})

Tactic:
exact (C_sub c.mem).left.inter <| (T1Space.t1 a).preimage X_cont

Goal state after: