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

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

Tactic:
by rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 Γ Λ σ
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
l : Λ
⊢ ∃ b,
    TrCfg (TM2.stepAux (M l) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (tr M (normal l)) v (Tape.mk' ∅ (addBottom L))) b

Tactic:
simp only [tr]

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
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
l : Λ
⊢ ∃ b,
    TrCfg (TM2.stepAux (M l) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (M l)) v (Tape.mk' ∅ (addBottom L))) b
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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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

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

Tactic:
by rintro ⟨⟨⟩⟩

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 rintro ⟨⟨⟩⟩

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

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

Tactic:
by rintro ⟨⟨⟩⟩

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

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

Tactic:
by rintro ⟨⟨⟩⟩

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

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

Tactic:
by rintro ⟨⟨⟩⟩

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

Goal state before:
pp: case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
⊢ (f.cons fs).Ok

Tactic:
intro k v; rw [stepNormal]

Goal state after:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
⊢ (f.comp g).Ok

Tactic:
intro k v; rw [stepNormal]

Goal state after:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal g (Cont.comp f k) v) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case case
f g : Code
IHf : f.Ok
IHg : g.Ok
⊢ (f.case g).Ok

Tactic:
intro k v; rw [stepNormal]

Goal state after:
case case
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI) k v) = do
    let v ← (f.case g).eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
f : Code
IHf : f.Ok
⊢ f.fix.Ok

Tactic:
intro k v; rw [stepNormal]

Goal state after:
case fix
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal f (Cont.fix f k) v) k v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case zero'
⊢ Code.zero'.Ok

Tactic:
intro k v; rw [stepNormal]

Goal state after:
case zero'
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k (0 :: v)) k v) = do
    let v ← Code.zero'.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case succ
⊢ Code.succ.Ok

Tactic:
intro k v; rw [stepNormal]

Goal state after:
case succ
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k [v.headI.succ]) k v) = do
    let v ← Code.succ.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case tail
⊢ Code.tail.Ok

Tactic:
intro k v; rw [stepNormal]

Goal state after:
case tail
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k v.tail) k v) = do
    let v ← Code.tail.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun z ↦ Classical.choose ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
⊢ (g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit

Tactic:
rw [comp_assoc, stoneCechExtend_extends ht, ← comp_assoc, hs, id_comp]

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
⊢ IsOpen (closure U)

Tactic:
have : CompactSpace Z := isCompact_iff_compactSpace.mp hZ.isCompact

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
⊢ IsOpen (closure U)
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
hsurj : Function.Surjective g
⊢ ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f

Tactic:
let A' : CompHaus := CompHaus.of A

Goal state after:
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
hsurj : Function.Surjective g
A' : CompHaus := of A
⊢ ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f
Module: Mathlib.Topology.DiscreteQuotient

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

Tactic:
by
        convert! isOpen_connectedComponent (x := x)
        ext y
        simpa only [connectedComponentSetoid, ← connectedComponent_eq_iff_mem] using! eq_comm

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

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

Tactic:
intro S E

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

Goal state before:
pp: C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
⊢ f = g

Tactic:
by
  apply Sheaf.hom_ext
  ext
  exact h _

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

Goal state before:
pp: I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
this✝ : (functor c).Initial
this : (StructuredArrow.toCostructuredArrow toProfinite c.pt).IsEquivalence
⊢ (functorOp c).Final

Tactic:
exact Functor.final_comp (functor c).op _

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
f✝ : β → γ
α✝ β✝ : Type u
f : Id (α✝ → β✝)
x : Id α✝
⊢ pure (f <*> x) = pure f <*> pure x

Tactic:
simp only [map_pure, seq_pure]

Goal state after:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
f✝ : β → γ
α✝ β✝ : Type u
f : Id (α✝ → β✝)
x : Id α✝
⊢ pure (f <*> x) = pure (f x)
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightProfinite
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite)
    (g : (free R).obj (P.toCondensed ⊗ S.toCondensed) ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P ⊗ S).toCondensed ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g = g' ≫ e

pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (P ⊗ S).toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P.toCondensed ⊗ S.toCondensed) ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e

Tactic:
· specialize h e S ((free R).map (μIso lightProfiniteToLightCondSet _ _).hom ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (free R).map (μIso
        lightProfiniteToLightCondSet _ _).inv ≫ g', ?_⟩
    rw [assoc, ← hh]
    simp [-map_comp, ← map_comp_assoc]

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (P ⊗ S).toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P.toCondensed ⊗ S.toCondensed) ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e