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

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ (↑(decode ((k (encode a)).get hk))).Dom

Tactic:
simp only [mem_map_iff, mem_coe, mem_bind_iff, Option.mem_def] at H

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
⊢ (↑(decode ((k (encode a)).get hk))).Dom
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℕ
⊢ ((move Dir.right)^[i] T).head = T.nth ↑i

Tactic:
induction i generalizing T

Goal state after:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ ((move Dir.right)^[0] T).head = T.nth ↑0

case succ
Γ : Type u_1
inst✝ : Inhabited Γ
n✝ : ℕ
a✝ : ∀ (T : Tape Γ), ((move Dir.right)^[n✝] T).head = T.nth ↑n✝
T : Tape Γ
⊢ ((move Dir.right)^[n✝ + 1] T).head = T.nth ↑(n✝ + 1)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : 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
⊢ Option.map (Cfg.map f₁ g₁) (step M { q := q, Tape := T }) =
    step (M.map f₁ f₂ g₁ g₂) (Cfg.map f₁ g₁ { q := q, Tape := T })

Tactic:
by
    unfold step Machine.map Cfg.map
    simp only [Turing.Tape.map_fst, g₂₁ q h, f₂₁ _]
    rcases M q T.1 with (_ | ⟨q', d | a⟩); · rfl
    · simp only [Option.map_some, Tape.map_move f₁]
      rfl
    · simp only [Option.map_some, Tape.map_write]
      rfl

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

Goal state before:
pp: case branch.true
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif true then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S

Tactic:
· exact IH₁ _ _ hs.1

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

Goal state before:
pp: case branch.true
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif true then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S

Tactic:
· exact IH₁ _ _ hs.1

Goal state after:
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
⊢ TM1.stepAux q (f v (some hd))
      ((Tape.move Dir.right)^[tl.length]
        (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a ↦ update a k none) tl.length L)))) =
    TM1.stepAux q (f v (some hd)) ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))

Tactic:
List.tail

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
⊢ TM1.stepAux q (f v (some hd))
      ((Tape.move Dir.right)^[tl.length]
        (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a ↦ update a k none) tl.length L)))) =
    TM1.stepAux q (f v (some hd)) ((Tape.move Dir.right)^[tl.length] (Tape.mk' ∅ (addBottom ?m.569)))
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 ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L))).head.1 then
      TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux q
        (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
        (Tape.write
          ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.1,
            update (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k
              none)
          (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (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:
erw [List.length_cons, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_succ_fst,
            cond_false, iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head,
            Tape.mk'_nth_nat, Tape.write_move_right_n fun a : Γ' K Γ ↦ (a.1, update a.2 k none),
            addBottom_modifyNth fun a ↦ update a k none, addBottom_nth_snd,
            stk_nth_val _ (hL k), e,
            show (List.cons hd tl).reverse[tl.length]? = some hd by
              rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length],
            List.head?, List.tail]

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case h_option
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
⊢ ∃ C,
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧ (∀ (i : Option I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C

Tactic:
have Z'_closed (i : I) : IsClosed (Z (some i)) := Z_closed (some i)

Goal state after:
case h_option
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
⊢ ∃ C,
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧ (∀ (i : Option I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
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
⊢ ∃ E, CompactSpace ↑E ∧ X '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X '' E₀ ≠ univ

Tactic:
let S : Set <| Set D := {E : Set D | IsClosed E ∧ X '' E = univ}

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}
⊢ ∃ E, CompactSpace ↑E ∧ X '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X '' E₀ ≠ univ
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ

Tactic:
disjoint_iff_inter_eq_empty,

Goal state after:
A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
⊢ (ρ '' G₁ᶜ)ᶜ ∩ (ρ '' G₂ᶜ)ᶜ = ∅
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: p : Γ' → Bool
k : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (L₁, o, L₂)
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
induction L₁ generalizing S s with
  | nil =>
    refine TransGen.head' rfl ?_
    rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
    revert e; rcases S k with - | ⟨a, Sk⟩ <;> intro e
    · cases e
      rfl
    simp only [splitAtPred, List.head?, List.tail_cons] at e ⊢
    revert e; cases p a <;> intro e <;>
      simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and, reduceCtorEq] at e ⊢
    rcases e with ⟨e₁, e₂⟩
    rw [e₁, e₂]
  | cons a L₁ IH =>
    refine TransGen.head rfl ?_
    rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
    rcases e₁ : S k with - | ⟨a', Sk⟩ <;> rw [e₁, splitAtPred] at e
    · cases e
    cases e₂ : p a' <;> simp only [e₂, cond] at e
    swap
    · cases e
    rcases e₃ : splitAtPred p Sk with ⟨_, _, _⟩
    rw [e₃] at e
    cases e
    simp only [List.head?_cons, e₂, List.tail_cons, cond_false]
    convert! @IH _ (update S k Sk) _ using 2 <;> simp [e₃]

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

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

Tactic:
rcases L₂ with - | ⟨a, L₂⟩

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

case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ Reaches₁ (TM2.step tr)
    { l := some (head stack q), var := s, stk := elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) }
    { l := some q, var := none, stk := elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃ }
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Profinite
⊢ Epi (π X)

Tactic:
have := (profiniteToCompHaus.obj X).projectivePresentation.epi
  rw [CompHaus.epi_iff_surjective] at this
  rw [epi_iff_surjective]
  exact this

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

Goal state before:
pp: case cons.succ
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).tail = trList ((n + 1) :: tail✝).tail
  else
    natEnd ((trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos (↑n).succ')).tail ++ Γ'.cons :: trList ((n + 1) :: tail✝).tail

Tactic:
List.tail

Goal state after:
case cons.succ
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos (↑n).succ')).tail ++ Γ'.cons :: trList tail✝
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case refine_1
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step tr) i
⊢ ∃ a ∈ c.eval v, halt a = x

Tactic:
obtain ⟨c, hc₁, hc₂⟩ := tr_eval_rev tr_respects h₁ h
    simp only [stepNormal_eval, Part.map_eq_map, Part.mem_map_iff] at hc₂
    obtain ⟨v', hv, rfl⟩ := hc₂
    exact ⟨_, hv, hc₁.symm⟩

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

Goal state before:
pp: case fix.true
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif true then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S

Tactic:
exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Sequence

Goal state before:
pp: case refine_1.some.some
n m : ℕ
h : natUnionInftyEmbedding (Option.some n) = natUnionInftyEmbedding (Option.some m)
⊢ Option.some n = Option.some m

Tactic:
simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_inj, add_left_inj,
        Nat.cast_inj] at h
      rw [h]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := 0 } ys).down = ys.length

Tactic:
rw [← Nat.add_zero ys.length]

Goal state after:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := 0 } ys).down = ys.length + 0
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case e_a.error
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
a✝ : ε
⊢ (callCC fun f ↦
      match Except.error a✝ with
      | Except.ok x => (next✝ (ExceptT.mkLabel f) x).run
      | Except.error e => pure (Except.error e)) =
    match Except.error a✝ with
    | Except.ok x => callCC fun x_1 ↦ (next✝ (ExceptT.mkLabel x_1) x).run
    | Except.error e => pure (Except.error e)

Tactic:
simp [@callCC_dummy m _]

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case e_a.ok
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
a✝ : α✝
⊢ (callCC fun f ↦
      match Except.ok a✝ with
      | Except.ok x => (next✝ (ExceptT.mkLabel f) x).run
      | Except.error e => pure (Except.error e)) =
    match Except.ok a✝ with
    | Except.ok x => callCC fun x_1 ↦ (next✝ (ExceptT.mkLabel x_1) x).run
    | Except.error e => pure (Except.error e)

Tactic:
simp [@callCC_dummy m _]

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
x✝¹ : OptionT m α✝
x✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (callCC fun f ↦ none.elim (pure none) fun x ↦ (x✝ (OptionT.mkLabel f) x).run) =
    none.elim (pure none) fun x ↦ callCC fun x_1 ↦ (x✝ (OptionT.mkLabel x_1) x).run

Tactic:
simp [@callCC_dummy m _]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix ⇑f = ωSup (approxChain f)

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix ⇑f ≤ ωSup (approxChain f)

case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ⇑f
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain { toFun := g, monotone' := ⋯ }) =
    ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ })

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain { toFun := g, monotone' := ⋯ }) ≤
    ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ })

case a
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) ≤
    ωSup (approxChain { toFun := g, monotone' := ⋯ })
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (α i)
s✝ : Finset ι
f✝ : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
f g : (a : ι) → a ∈ s → α a
h : (fun i ↦ f ↑i ⋯) = fun i ↦ g ↑i ⋯
⊢ f = g

Tactic:
ext i hi

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (α i)
s✝ : Finset ι
f✝ : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
f g : (a : ι) → a ∈ s → α a
h : (fun i ↦ f ↑i ⋯) = fun i ↦ g ↑i ⋯
i : ι
hi : i ∈ s
⊢ f i hi = g i hi
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m n : ℕ
f : Fin m → Fin n
hf : Function.Surjective f
⊢ n ≤ m

Tactic:
simpa using Fintype.card_le_of_surjective f hf

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case neg
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ¬↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

Tactic:
simp only [h', ↓reduceDIte, subNat, castLE, Fin.cast, eqRec_eq_cast]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
⊢ ∀ (x : Sigma β), x ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)

Tactic:
by intro x; cases x; simp

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

Goal state before:
pp: α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ lookmap f l = l

Tactic:
rw [← map_id (l.lookmap f), lookmap_map_eq, map_id]; exact h

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ (kextract a s.entries).snd.NodupKeys

Tactic:
rw [kextract_eq_dlookup_kerase]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ (dlookup a s.entries, kerase a s.entries).snd.NodupKeys
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

Tactic:
· left
          rw [h'.2]

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

Goal state before:
pp: case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

Tactic:
· left
          rw [h'.2]

Goal state after: