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

Goal state before:
pp: case none
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (TM2.stepAux
      (branch (fun s ↦ (id s).isSome)
        (push k₁ (fun s ↦ (id s).getD default) (goto fun x ↦ Λ'.move (fun x ↦ false) rev k₂ q))
        (goto fun x ↦ Λ'.move (fun x ↦ false) rev k₂ q))
      none (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (id L₂)) k₂ (L₁ ++ S k₂) }

pp: case some
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (TM2.stepAux
      (branch (fun s ↦ (id s).isSome)
        (push k₁ (fun s ↦ (id s).getD default) (goto fun x ↦ Λ'.move (fun x ↦ false) rev k₂ q))
        (goto fun x ↦ Λ'.move (fun x ↦ false) rev k₂ q))
      (some val✝) (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) }

Tactic:
<;>

Goal state after:
case none
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (TM2.stepAux
      (branch (fun s ↦ (id s).isSome)
        (push k₁ (fun s ↦ (id s).getD default) (goto fun x ↦ Λ'.move (fun x ↦ false) rev k₂ q))
        (goto fun x ↦ Λ'.move (fun x ↦ false) rev k₂ q))
      none (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (id L₂)) k₂ (L₁ ++ S k₂) }

case some
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (TM2.stepAux
      (branch (fun s ↦ (id s).isSome)
        (push k₁ (fun s ↦ (id s).getD default) (goto fun x ↦ Λ'.move (fun x ↦ false) rev k₂ q))
        (goto fun x ↦ Λ'.move (fun x ↦ false) rev k₂ q))
      (some val✝) (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil.nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
⊢ splitAtPred p [] = ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif
          match [].head?, true, p with
          | some x, x_1, f => f x
          | none, y, x => y then
        { l := some q, var := [].head?, stk := update S k [].tail }
      else { l := some (Λ'.clear p k q), var := [].head?, stk := update S k [].tail })
      { l := some q, var := o, stk := update S k L₂ }

pp: case nil.cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ splitAtPred p (a :: Sk) = ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif
          match (a :: Sk).head?, true, p with
          | some x, x_1, f => f x
          | none, y, x => y then
        { l := some q, var := (a :: Sk).head?, stk := update S k (a :: Sk).tail }
      else { l := some (Λ'.clear p k q), var := (a :: Sk).head?, stk := update S k (a :: Sk).tail })
      { l := some q, var := o, stk := update S k L₂ }

Tactic:
<;>

Goal state after:
case nil.nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
⊢ splitAtPred p [] = ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif
          match [].head?, true, p with
          | some x, x_1, f => f x
          | none, y, x => y then
        { l := some q, var := [].head?, stk := update S k [].tail }
      else { l := some (Λ'.clear p k q), var := [].head?, stk := update S k [].tail })
      { l := some q, var := o, stk := update S k L₂ }

case nil.cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ splitAtPred p (a :: Sk) = ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif
          match (a :: Sk).head?, true, p with
          | some x, x_1, f => f x
          | none, y, x => y then
        { l := some q, var := (a :: Sk).head?, stk := update S k (a :: Sk).tail }
      else { l := some (Λ'.clear p k q), var := (a :: Sk).head?, stk := update S k (a :: Sk).tail })
      { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil.cons.false
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ (bif false then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif false then { l := some q, var := some a, stk := update S k Sk }
      else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
      { l := some q, var := o, stk := update S k L₂ }

pp: case nil.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ (bif true then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif true then { l := some q, var := some a, stk := update S k Sk }
      else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
      { l := some q, var := o, stk := update S k L₂ }

Tactic:
<;>

Goal state after:
case nil.cons.false
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ (bif false then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif false then { l := some q, var := some a, stk := update S k Sk }
      else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
      { l := some q, var := o, stk := update S k L₂ }

case nil.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ (bif true then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif true then { l := some q, var := some a, stk := update S k Sk }
      else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
      { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil.cons.false
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e :
  (bif false then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
    ([], o, L₂)
⊢ ReflTransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif false then { l := some q, var := some a, stk := update S k Sk }
    else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
    { l := some q, var := o, stk := update S k L₂ }

pp: case nil.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e :
  (bif true then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
    ([], o, L₂)
⊢ ReflTransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif true then { l := some q, var := some a, stk := update S k Sk }
    else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
<;>

Goal state after:
case nil.cons.false
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e :
  (bif false then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
    ([], o, L₂)
⊢ ReflTransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif false then { l := some q, var := some a, stk := update S k Sk }
    else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
    { l := some q, var := o, stk := update S k L₂ }

case nil.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e :
  (bif true then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
    ([], o, L₂)
⊢ ReflTransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif true then { l := some q, var := some a, stk := update S k Sk }
    else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
    { l := some q, var := o, stk := update S k L₂ }
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₂
⊢ False

Tactic:
rcases t2_separation hx with ⟨G₁, G₂, G₁_open, G₂_open, hx₁, hx₂, disj⟩

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₂
⊢ False
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_2
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1, stk := update S k (fst✝¹, fst✝, snd✝).2.2 }
⊢ update S k snd✝ = update (update S k Sk) k (fst✝¹, fst✝, snd✝).2.2

pp: case cons.cons.false.refl.convert_2
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1, stk := update S k (fst✝¹, fst✝, snd✝).2.2 }
⊢ splitAtPred p (update S k Sk k) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2)

Tactic:
<;>

Goal state after:
case e'_2
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1, stk := update S k (fst✝¹, fst✝, snd✝).2.2 }
⊢ update S k snd✝ = update (update S k Sk) k (fst✝¹, fst✝, snd✝).2.2

case cons.cons.false.refl.convert_2
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1, stk := update S k (fst✝¹, fst✝, snd✝).2.2 }
⊢ splitAtPred p (update S k Sk k) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case refine_1.nil
q : Λ'
s : Option Γ'
c d : List Γ'
o : Option Γ' := List.casesOn [] none fun x x_1 ↦ some Γ'.cons
⊢ Option.elim' (elim (trList []) [] c d main = trNat [].headI ∧ trList [].tail = [])
    (fun a ↦ natEnd a = true ∧ elim (trList []) [] c d main = trNat [].headI ++ a :: trList [].tail) o

pp: case refine_1.cons
q : Λ'
s : Option Γ'
c d : List Γ'
head✝ : ℕ
tail✝ : List ℕ
o : Option Γ' := List.casesOn (head✝ :: tail✝) none fun x x_1 ↦ some Γ'.cons
⊢ Option.elim'
    (elim (trList (head✝ :: tail✝)) [] c d main = trNat (head✝ :: tail✝).headI ∧ trList (head✝ :: tail✝).tail = [])
    (fun a ↦
      natEnd a = true ∧
        elim (trList (head✝ :: tail✝)) [] c d main = trNat (head✝ :: tail✝).headI ++ a :: trList (head✝ :: tail✝).tail)
    o

Tactic:
<;>

Goal state after:
case refine_1.nil
q : Λ'
s : Option Γ'
c d : List Γ'
o : Option Γ' := List.casesOn [] none fun x x_1 ↦ some Γ'.cons
⊢ Option.elim' (elim (trList []) [] c d main = trNat [].headI ∧ trList [].tail = [])
    (fun a ↦ natEnd a = true ∧ elim (trList []) [] c d main = trNat [].headI ++ a :: trList [].tail) o

case refine_1.cons
q : Λ'
s : Option Γ'
c d : List Γ'
head✝ : ℕ
tail✝ : List ℕ
o : Option Γ' := List.casesOn (head✝ :: tail✝) none fun x x_1 ↦ some Γ'.cons
⊢ Option.elim'
    (elim (trList (head✝ :: tail✝)) [] c d main = trNat (head✝ :: tail✝).headI ∧ trList (head✝ :: tail✝).tail = [])
    (fun a ↦
      natEnd a = true ∧
        elim (trList (head✝ :: tail✝)) [] c d main = trNat (head✝ :: tail✝).headI ++ a :: trList (head✝ :: tail✝).tail)
    o
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil
q : Λ'
s : Option Γ'
c d : List Γ'
o : Option Γ' := List.casesOn [] none fun x x_1 ↦ some Γ'.cons
⊢ o ≠ some Γ'.consₗ

pp: case cons
q : Λ'
s : Option Γ'
c d : List Γ'
head✝ : ℕ
tail✝ : List ℕ
o : Option Γ' := List.casesOn (head✝ :: tail✝) none fun x x_1 ↦ some Γ'.cons
⊢ o ≠ some Γ'.consₗ

Tactic:
<;>

Goal state after:
case nil
q : Λ'
s : Option Γ'
c d : List Γ'
o : Option Γ' := List.casesOn [] none fun x x_1 ↦ some Γ'.cons
⊢ o ≠ some Γ'.consₗ

case cons
q : Λ'
s : Option Γ'
c d : List Γ'
head✝ : ℕ
tail✝ : List ℕ
o : Option Γ' := List.casesOn (head✝ :: tail✝) none fun x x_1 ↦ some Γ'.cons
⊢ o ≠ some Γ'.consₗ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case one
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum PosNum.one) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum PosNum.one.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ ∃ a l, trPosNum PosNum.one = a :: l ∧ natEnd a = false

pp: case bit1
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
a✝ : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a✝.bit1) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a✝.bit1.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ ∃ a l, trPosNum a✝.bit1 = a :: l ∧ natEnd a = false

pp: case bit0
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
a✝ : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a✝.bit0) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a✝.bit0.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ ∃ a l, trPosNum a✝.bit0 = a :: l ∧ natEnd a = false

Tactic:
<;>

Goal state after:
case one
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum PosNum.one) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum PosNum.one.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ ∃ a l, trPosNum PosNum.one = a :: l ∧ natEnd a = false

case bit1
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
a✝ : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a✝.bit1) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a✝.bit1.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ ∃ a l, trPosNum a✝.bit1 = a :: l ∧ natEnd a = false

case bit0
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
a✝ : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a✝.bit0) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a✝.bit0.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ ∃ a l, trPosNum a✝.bit0 = a :: l ∧ natEnd a = false
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q₁ q₂ : Λ'
s : Option Γ'
v : List ℕ
c d : List Γ'
⊢ ∃ s',
    Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trList v) [] c d }
      (Nat.rec { l := some q₁, var := s', stk := elim (trList v.tail) [] c d }
        (fun n x ↦ { l := some q₂, var := s', stk := elim (trList (n :: v.tail)) [] c d }) v.headI)

Tactic:
by
  rcases v with (_ | ⟨_ | n, v⟩)
  · refine ⟨none, TransGen.single ?_⟩
    simp
  · refine ⟨some Γ'.cons, TransGen.single ?_⟩
    simp
  refine ⟨none, ?_⟩
  simp only [trList, trNat.eq_1, trNum, Nat.cast_succ, Num.add_one, Num.succ,
    List.tail_cons, List.headI_cons]
  rcases (n : Num) with - | a
  · simp only [trPosNum, Num.succ', List.singleton_append, List.nil_append]
    refine TransGen.head rfl ?_
    rw [tr]; simp only [pop', TM2.stepAux]
    convert! unrev_ok using 2
    simp
  simp only [Num.succ']
  suffices ∀ l₁, ∃ l₁' l₂' s',
    List.reverseAux l₁ (trPosNum a) = List.reverseAux l₁' l₂' ∧
      Reaches₁ (TM2.step tr)
        ⟨some (q₁.pred q₂), s, K'.elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d⟩
        ⟨some (unrev q₂), s', K'.elim (l₂' ++ Γ'.cons :: trList v) l₁' c d⟩ by
    obtain ⟨l₁', l₂', s', e, h⟩ := this []
    simp only [List.reverseAux] at e
    refine h.trans ?_
    convert! unrev_ok using 2
    simp [e, List.reverseAux_eq]
  induction a generalizing s with intro l₁
  | one =>
    refine ⟨Γ'.bit1::l₁, [], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
    simp [trPosNum, show PosNum.one.succ = PosNum.one.bit0 from rfl]
  | bit1 m IH =>
    obtain ⟨l₁', l₂', s', e, h⟩ := IH (some Γ'.bit0) (Γ'.bit1 :: l₁)
    refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
    simp
    rfl
  | bit0 m IH =>
    obtain ⟨a, l, e, h⟩ : ∃ a l, (trPosNum m = a::l) ∧ natEnd a = false := by
      cases m <;> refine ⟨_, _, rfl, rfl⟩
    refine ⟨Γ'.bit0 :: l₁, _, some a, rfl, TransGen.single ?_⟩
    simp [trPosNum, PosNum.succ, e, h, show some Γ'.bit1 ≠ some Γ'.bit0 by decide,
      Option.getD, -natEnd]
    rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case pos
α : 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
A : Set X
h : IsClopen A
x : X
hx : x ∈ A
⊢ IsOpen[inst✝²] (ofPred ((fun x y ↦ x ∈ A ↔ y ∈ A) x))

pp: case neg
α : 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
A : Set X
h : IsClopen A
x : X
hx : x ∉ A
⊢ IsOpen[inst✝²] (ofPred ((fun x y ↦ x ∈ A ↔ y ∈ A) x))

Tactic:
<;>

Goal state after:
case pos
α : 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
A : Set X
h : IsClopen A
x : X
hx : x ∈ A
⊢ IsOpen[inst✝²] (ofPred ((fun x y ↦ x ∈ A ↔ y ∈ A) x))

case neg
α : 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
A : Set X
h : IsClopen A
x : X
hx : x ∉ A
⊢ IsOpen[inst✝²] (ofPred ((fun x y ↦ x ∈ A ↔ y ∈ A) x))