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

Goal state before:
pp: a b : Num
⊢ ↑a ≤ ↑b ∨ ↑b ≤ ↑a

Tactic:
apply le_total

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
x : List α
⊢ x ∈ M.accepts → ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'

Tactic:
intro ⟨s₂, _, h⟩

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left✝ : s₂ ∈ M.accept
h : s₂ ∈ M.eval x
⊢ ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
a b : PosNum
⊢ ↑a ≤ ↑b ∨ ↑b ≤ ↑a

Tactic:
apply le_total

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ x✝ ∈ M.toεNFA.stepSet S s ↔ x✝ ∈ M.stepSet S s

Tactic:
simp only [stepSet, εNFA.stepSet, exists_prop, Set.mem_iUnion]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ (∃ i ∈ S, x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step i (some s))) ↔ ∃ i ∈ S, x✝ ∈ M.step i s
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ ↑n.bit0 + ↑1 = 2 * ↑n + 1

Tactic:
cast_bit0

Goal state after:
α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ 2 * ↑n + ↑1 = 2 * ↑n + 1
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l l₁ l₂ : List Γ
⊢ BlankExtends l₁ l → BlankExtends l₂ l → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

Tactic:
by
  rintro ⟨i, rfl⟩ ⟨j, e⟩ h; use i - j
  refine List.append_cancel_right (e.symm.trans ?_)
  rw [List.append_assoc, ← List.replicate_add, Nat.sub_add_cancel]
  apply_fun List.length at e
  simp only [List.length_append, List.length_replicate] at e
  rwa [← Nat.add_le_add_iff_left, e, Nat.add_le_add_iff_right]

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

Goal state before:
pp: case zero.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L : ListBlank Γ
⊢ (modifyNth f 0 L).nth 0 = if 0 = 0 then f (L.nth 0) else L.nth 0

Tactic:
simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth,
      ListBlank.nth_succ, if_false, ListBlank.tail_cons, reduceCtorEq]

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

Goal state before:
pp: case zero.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L : ListBlank Γ
n✝ : ℕ
⊢ (modifyNth f 0 L).nth (n✝ + 1) = if n✝ + 1 = 0 then f (L.nth (n✝ + 1)) else L.nth (n✝ + 1)

Tactic:
simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth,
      ListBlank.nth_succ, if_false, ListBlank.tail_cons, reduceCtorEq]

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₂
e : σ₂
h : e ∈ f₂ b₂
right✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) e d₂
⊢ some d₁ = none

Tactic:
cases b0.symm.trans h

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
hf : ∀ (a : Γ), SupportsStmt S (f✝ a)
⊢ ∀ (v : List.Vector Bool n), SupportsStmt S (move n Dir.left (f✝ (dec v)))

Tactic:
intro; simp only [supportsStmt_move, hf]

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

Goal state before:
pp: tm : FinTM2
s : List (tm.Γ tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (tm.Γ k)

Tactic:
by rw [h]; exact s

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

Goal state before:
pp: tm : FinTM2
s : List (tm.Γ tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (tm.Γ k)

Tactic:
by rw [h]; exact s

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

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

Tactic:
unfold writes at hw ⊢

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

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

Tactic:
unfold writes at hw ⊢

Goal state after:
case write
Γ : 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
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  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')
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ q' ∈ Finset.image (fun a ↦ Λ'.write a q) Finset.univ ∪ writes q, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
    ∀ q' ∈ Finset.image (fun a ↦ Λ'.write a q) Finset.univ ∪ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
unfold writes at hw ⊢

Goal state after:
case load
Γ : 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
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH :
  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')
hs : SupportsStmt S (Stmt.load a q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.load a q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
unfold writes at hw ⊢

Goal state after:
case branch
Γ : 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
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  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')
IH₂ :
  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')
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ q' ∈ writes q₁ ∪ writes q₂, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
    ∀ q' ∈ writes q₁ ∪ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
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))
i : ℕ
h : ¬i = (S k).length
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
rcases lt_or_gt_of_ne h with h | h

Goal state after:
case neg.inl
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
h : i < (S k).length
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

case neg.inr
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
h : (S k).length < i
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i
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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ (bif ((addBottom L).nth (tl.length + 1)).1 then
      TM1.stepAux q (f v none) ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux q
        (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))).head.2 k))
        (Tape.write
          ((Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))).head.1,
            update (Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))).head.2 k
              none)
          (Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))))) =
    TM1.stepAux q (f v (hd :: tl).head?)
      ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))

Tactic:
addBottom_nth_succ_fst,

Goal state after:
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
⊢ (bif false then TM1.stepAux q (f v none) ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux q
        (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))).head.2 k))
        (Tape.write
          ((Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))).head.1,
            update (Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))).head.2 k
              none)
          (Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))))) =
    TM1.stepAux q (f v (hd :: tl).head?)
      ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))
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
i : ℕ
h : ¬i = tl.length
⊢ ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.getI i

Tactic:
rcases lt_or_gt_of_ne h with h | h

Goal state after:
case neg.inl
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
i : ℕ
h✝ : ¬i = tl.length
h : i < tl.length
⊢ ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.getI i

case neg.inr
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
i : ℕ
h✝ : ¬i = tl.length
h : tl.length < i
⊢ ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.getI i
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
P' : TopCat → Prop
h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop
⊢ PreservesLimit (cospan f g) (toCompHausLike h)

Tactic:
have : PreservesLimit (cospan f g) (toCompHausLike h ⋙ compHausLikeToTop P') :=
    inferInstanceAs (PreservesLimit _ (compHausLikeToTop _))
  exact preservesLimit_of_reflects_of_preserves (toCompHausLike h) (compHausLikeToTop P')

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

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif ((addBottom L).nth (n + 1)).1 then
      TM1.stepAux (trNormal q) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux (move Dir.left (goto fun x x_1 ↦ ret q)) v
        ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }

Tactic:
addBottom_nth_succ_fst,

Goal state after:
case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif false then TM1.stepAux (trNormal q) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux (move Dir.left (goto fun x x_1 ↦ ret q)) v
        ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: ⊢ trNat 0 = []

Tactic:
rw [trNat, Nat.cast_zero]

Goal state after:
⊢ trNum 0 = []
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ (∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)) → x ∈ eval step (stepNormal f (Cont.fix f k) v)

Tactic:
rintro ⟨v', he, hr⟩

Goal state after:
case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_1.inl.inl.peek
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
k✝ : K
q✝ : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Option (Γ k✝) → σ
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ (StAct.peek a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.peek a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.peek a✝) q✝))

pp: case refine_1.inl.inl.pop
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
k✝ : K
q✝ : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Option (Γ k✝) → σ
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ (StAct.pop a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.pop a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.pop a✝) q✝))

Tactic:
· exact ⟨fun _ _ ↦ hret, fun _ _ ↦ hgo⟩

Goal state after:
case refine_1.inl.inl.pop
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
k✝ : K
q✝ : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Option (Γ k✝) → σ
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ (StAct.pop a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.pop a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.pop a✝) q✝))
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: 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}
this : ∀ C ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x ↦ x ∈ S) E
⊢ ∃ E, CompactSpace ↑E ∧ X '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X '' E₀ ≠ univ

Tactic:
obtain ⟨E_closed, E_surj⟩ := E_min.prop

Goal state after:
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}
this : ∀ C ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x ↦ x ∈ S) E
E_closed : IsClosed E
E_surj : X '' E = univ
⊢ ∃ E, CompactSpace ↑E ∧ X '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X '' E₀ ≠ univ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ Reaches₁ (TM2.step tr)
    { l := some (head stack q), var := s, stk := elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) }
    { l := some q, var := none, stk := elim (trList ([].headI :: L₁)) [] [] L₃ }

Tactic:
refine
      TransGen.trans
        (move_ok (by decide)
          (splitAtPred_eq _ _ [] (some Γ'.consₗ) L₃ (by rintro _ ⟨⟩) ⟨rfl, rfl⟩))
        (TransGen.head rfl (TransGen.head rfl ?_))
    rw [tr]
    simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_true, id_eq, trList, List.nil_append,
      elim_update_stack, elim_rev, List.reverseAux_nil, elim_update_rev, Function.update_self,
      List.headI_nil, trNat_default]
    convert! unrev_ok using 2
    simp

Goal state after: