mathlib-initiative/mathlib-tactics huggingface dataset:
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 Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b
⊢ ∃ b,
    TrCfg (TM2.stepAux (stRun o q) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (stRun o q)) v (Tape.mk' ∅ (addBottom T))) b

Tactic:
by

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
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b
⊢ ∃ b,
    TrCfg (TM2.stepAux (stRun o q) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (stRun o q)) v (Tape.mk' ∅ (addBottom T))) b

Tactic:
by
  simp only [trNormal_run, step_run]
  have hgo := tr_respects_aux₁ M o q v (hT k) _ le_rfl
  obtain ⟨T', hT', hrun⟩ := tr_respects_aux₂ (Λ := Λ) hT o
  have := hgo.tail' rfl
  rw [tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd,
    stk_nth_val _ (hT k), List.getElem?_eq_none (le_of_eq List.length_reverse),
    Option.isNone, cond, hrun, TM1.stepAux] at this
  obtain ⟨c, gc, rc⟩ := IH hT'
  refine ⟨c, gc, (this.to₀.trans (tr_respects_aux₃ M _) c (TransGen.head' rfl ?_)).to_reflTransGen⟩
  rw [tr, TM1.stepAux, Tape.mk'_head, addBottom_head_fst]
  exact rc

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

Goal state before:
pp: p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ ¬move p✝ k₁✝ k₂✝ q✝ = q₁✝.pred q₂✝

Tactic:
by

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

Goal state before:
pp: p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ ¬move p✝ k₁✝ k₂✝ q✝ = ret k✝

Tactic:
by

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

Goal state before:
pp: p✝¹ : Γ' → Bool
k✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ ¬clear p✝¹ k✝ q✝¹ = move p✝ k₁✝ k₂✝ q✝

Tactic:
by

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

Goal state before:
pp: p✝ : Γ' → Bool
k✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ ¬clear p✝ k✝ q✝¹ = q✝.copy

Tactic:
by

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

Goal state before:
pp: p✝ : Γ' → Bool
k✝¹ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ ¬clear p✝ k✝¹ q✝¹ = push k✝ s✝ q✝

Tactic:
by

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

Goal state before:
pp: p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ ¬clear p✝ k✝ q✝ = read f✝

Tactic:
by

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

Goal state before:
pp: p✝ : Γ' → Bool
k✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ ¬clear p✝ k✝ q✝¹ = q✝.succ

Tactic:
by

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

Goal state before:
pp: p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ ¬clear p✝ k✝ q✝ = q₁✝.pred q₂✝

Tactic:
by

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

Goal state before:
pp: p✝ : Γ' → Bool
k✝¹ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ ¬clear p✝ k✝¹ q✝ = ret k✝

Tactic:
by

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

Goal state before:
pp: q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ ¬q✝¹.copy = move p✝ k₁✝ k₂✝ q✝

Tactic:
by

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

Goal state before:
pp: q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ ¬q✝¹.copy = clear p✝ k✝ q✝

Tactic:
by

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

Goal state before:
pp: q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ ¬q✝¹.copy = push k✝ s✝ q✝

Tactic:
by

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

Goal state before:
pp: q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ ¬q✝.copy = read f✝

Tactic:
by

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

Goal state before:
pp: q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ ¬q✝¹.copy = q✝.succ

Tactic:
by

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

Goal state before:
pp: q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ ¬q✝.copy = q₁✝.pred q₂✝

Tactic:
by

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

Goal state before:
pp: q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ ¬q✝.copy = ret k✝

Tactic:
by

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

Goal state before:
pp: k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ ¬push k✝ s✝ q✝¹ = move p✝ k₁✝ k₂✝ q✝

Tactic:
by

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

Goal state before:
pp: k✝¹ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ ¬push k✝¹ s✝ q✝¹ = clear p✝ k✝ q✝

Tactic:
by

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

Goal state before:
pp: k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ ¬push k✝ s✝ q✝¹ = q✝.copy

Tactic:
by

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

Goal state before:
pp: k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ ¬push k✝ s✝ q✝ = read f✝

Tactic:
by

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

Goal state before:
pp: k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ ¬push k✝ s✝ q✝¹ = q✝.succ

Tactic:
by

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

Goal state before:
pp: k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ ¬push k✝ s✝ q✝ = q₁✝.pred q₂✝

Tactic:
by

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

Goal state before:
pp: k✝¹ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ ¬push k✝¹ s✝ q✝ = ret k✝

Tactic:
by

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

Goal state before:
pp: f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ ¬read f✝ = move p✝ k₁✝ k₂✝ q✝

Tactic:
by

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

Goal state before:
pp: f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ ¬read f✝ = clear p✝ k✝ q✝

Tactic:
by

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

Goal state before:
pp: f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q✝ : Λ'
⊢ ¬read f✝ = q✝.copy

Tactic:
by

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

Goal state before:
pp: f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ ¬read f✝ = push k✝ s✝ q✝

Tactic:
by

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

Goal state before:
pp: f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q✝ : Λ'
⊢ ¬read f✝ = q✝.succ

Tactic:
by

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

Goal state before:
pp: f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q₁✝ q₂✝ : Λ'
⊢ ¬read f✝ = q₁✝.pred q₂✝

Tactic:
by

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

Goal state before:
pp: f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
k✝ : Cont'
⊢ ¬read f✝ = ret k✝

Tactic:
by

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

Goal state before:
pp: q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ ¬q✝¹.succ = move p✝ k₁✝ k₂✝ q✝

Tactic:
by

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

Goal state before:
pp: q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ ¬q✝¹.succ = clear p✝ k✝ q✝

Tactic:
by

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

Goal state before:
pp: q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ ¬q✝¹.succ = q✝.copy

Tactic:
by

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

Goal state before:
pp: q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ ¬q✝¹.succ = push k✝ s✝ q✝

Tactic:
by

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

Goal state before:
pp: q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ ¬q✝.succ = read f✝

Tactic:
by

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

Goal state before:
pp: q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ ¬q✝.succ = q₁✝.pred q₂✝

Tactic:
by

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

Goal state before:
pp: q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ ¬q✝.succ = ret k✝

Tactic:
by

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

Goal state before:
pp: q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ ¬q₁✝.pred q₂✝ = move p✝ k₁✝ k₂✝ q✝

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
h : IsTopologicalBasis {s | IsClopen s}
⊢ TotallySeparatedSpace X

Tactic:
by

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

Goal state before:
pp: q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ ¬q₁✝.pred q₂✝ = clear p✝ k✝ q✝

Tactic:
by

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

Goal state before:
pp: q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
q✝ : Λ'
⊢ ¬q₁✝.pred q₂✝ = q✝.copy

Tactic:
by

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

Goal state before:
pp: q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ ¬q₁✝.pred q₂✝ = push k✝ s✝ q✝

Tactic:
by

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

Goal state before:
pp: q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
f✝ : Option Γ' → Λ'
⊢ ¬q₁✝.pred q₂✝ = read f✝

Tactic:
by

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

Goal state before:
pp: q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
q✝ : Λ'
⊢ ¬q₁✝.pred q₂✝ = q✝.succ

Tactic:
by

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

Goal state before:
pp: q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
k✝ : Cont'
⊢ ¬q₁✝.pred q₂✝ = ret k✝

Tactic:
by

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

Goal state before:
pp: k✝ : Cont'
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ ¬ret k✝ = move p✝ k₁✝ k₂✝ q✝

Tactic:
by

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

Goal state before:
pp: k✝¹ : Cont'
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ ¬ret k✝¹ = clear p✝ k✝ q✝

Tactic:
by

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

Goal state before:
pp: k✝ : Cont'
q✝ : Λ'
⊢ ¬ret k✝ = q✝.copy

Tactic:
by

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

Goal state before:
pp: k✝¹ : Cont'
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ ¬ret k✝¹ = push k✝ s✝ q✝

Tactic:
by

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

Goal state before:
pp: k✝ : Cont'
f✝ : Option Γ' → Λ'
⊢ ¬ret k✝ = read f✝

Tactic:
by

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

Goal state before:
pp: k✝ : Cont'
q✝ : Λ'
⊢ ¬ret k✝ = q✝.succ

Tactic:
by

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

Goal state before:
pp: k✝ : Cont'
q₁✝ q₂✝ : Λ'
⊢ ¬ret k✝ = q₁✝.pred q₂✝

Tactic:
by

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

Goal state before:
pp: case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ ∃ b,
    TrCfg (TM2.stepAux TM2.Stmt.halt v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal TM2.Stmt.halt) v (Tape.mk' ∅ (addBottom L))) b

Tactic:
| halt =>

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
M : Λ → TM2.Stmt Γ Λ σ
⊢ Respects (TM2.step M) (TM1.step (tr M)) TrCfg

Tactic:
by

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

Goal state before:
pp: a b : Λ'
⊢ Decidable (a = b)

Tactic:
by

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

Goal state before:
pp: 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 }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst✝³] ↑s
⊢ Directed GE.ge fun s ↦ ↑s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b c d a' : List Γ'
⊢ update (elim a b c d) main a' = elim a' b c d

Tactic:
by

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

Goal state before:
pp: 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 }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst✝³] ↑s
hdir : Directed GE.ge fun s ↦ ↑s
y : X
y_in : y = x
⊢ U ∈ 𝓝 y

Tactic:
rwa [y_in]

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

Goal state before:
pp: 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 }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst✝³] ↑s
hdir : Directed GE.ge fun s ↦ ↑s
y : X
y_in : y ∈ ⋂ s, ↑s
⊢ U ∈ 𝓝 y

Tactic:
by

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

Goal state before:
pp: a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' = elim a b' c d

Tactic:
by

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

Goal state before:
pp: a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' = elim a b c' d

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
⊢ U ∈ 𝓝 x ↔ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
by

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

Goal state before:
pp: a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' = elim a b c d'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l₁ : List α
o : α
l₂ : List α
x✝ : ∀ x ∈ l₁, p x = false
left✝ : p o = true
h₃ : [] = l₁ ++ o :: l₂
⊢ splitAtPred p [] = (l₁, some o, l₂)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
⊢ IsTopologicalBasis {s | IsClopen s}

Tactic:
by

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

Goal state before:
pp: f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
⊢ step (stepRet (Cont.fix f k) v') = some (stepRet (k₀.then (Cont.fix f k)) v₀)

Tactic:
by

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

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
⊢ (range fun x ↦ ↑↑x) = interior s

Tactic:
by

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

Goal state before:
pp: f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
⊢ Reaches step (stepNormal f Cont.halt v'.tail) (stepRet k₀ v₀)

Tactic:
by

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

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
⊢ IsOpenEmbedding fun x ↦ ↑↑x

Tactic:
by

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

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
f1 : IsOpenEmbedding fun x ↦ ↑↑x
f2 : IsOpen[instTopologicalSpaceSubtype] v
⊢ Subtype.val '' V = (fun x ↦ ↑↑x) '' v

Tactic:
by

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

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ IsClopen (Subtype.val '' V)

Tactic:
by

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

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
VisClopen' : IsClopen (Subtype.val '' V)
⊢ ↑x ∈ Subtype.val '' V

Tactic:
by

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

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
VisClopen' : IsClopen (Subtype.val '' V)
⊢ Subtype.val '' V ⊆ s

Tactic:
by

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

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
⊢ IsTopologicalBasis {s | IsClopen s}

Tactic:
by

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

Goal state before:
pp: H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H

Tactic:
by

Goal state after: