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

Goal state before:
pp: h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
this : 0 < log x
⊢ 0 < 1 + ε x

Tactic:
change 0 < 1 + 1 / log x

Goal state after:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
this : 0 < log x
⊢ 0 < 1 + 1 / log x
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
⊢ [Symbol.nonterminal t] ≠ s ∧ ∀ (v : List (Symbol T g.NT)), g.Produces [Symbol.nonterminal t] v → ¬g.Derives v s

Tactic:
refine ⟨hs.symm, fun _ hx ↦ ?_⟩

Goal state after:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
x✝ : List (Symbol T g.NT)
hx : g.Produces [Symbol.nonterminal t] x✝
⊢ ¬g.Derives x✝ s
Module: Mathlib.Computability.DFA

Goal state before:
pp: case refine_2
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ (List.take (↑n) (List.take (↑m) x)).length + (List.drop (↑n) (List.take (↑m) x)).length ≤ Fintype.card σ

Tactic:
simp only [List.length_drop, List.length_take]

Goal state after:
case refine_2
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ min (↑n) (min (↑m) x.length) + (min (↑m) x.length - ↑n) ≤ Fintype.card σ
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case pos.true
m n : ℕ
IH : shiftLeft' true m n ≠ 0 → (shiftLeft' true m n).size = m.size + n
h : ¬bit true 0 = 0
s0 : shiftLeft' true m n = 0
this : (m + 1) * 2 ^ n = 1
⊢ (size 0).succ = (m.size + n).succ

Tactic:
obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)

Goal state after:
case pos.true
n : ℕ
h : ¬bit true 0 = 0
IH : shiftLeft' true 0 n ≠ 0 → (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : (0 + 1) * 2 ^ n = 1
⊢ (size 0).succ = (size 0 + n).succ
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: b : Bool
m n : ℕ
h : shiftLeft' b m n ≠ 0
⊢ (shiftLeft' b m n).size = m.size + n

Tactic:
induction n with
  | zero => simp [shiftLeft']
  | succ n IH =>
    simp only [shiftLeft', ne_eq] at h ⊢
    rw [size_bit h, Nat.add_succ]
    by_cases s0 : shiftLeft' b m n = 0
    case neg => rw [IH s0]
    rw [s0] at h ⊢
    cases b; · exact absurd rfl h
    have : shiftLeft' true m n + 1 = 1 := congr_arg (· + 1) s0
    rw [shiftLeft'_true_eq_mul_pow] at this
    obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
    simp only [Nat.zero_add, Nat.one_mul, Nat.pow_eq_one, succ_ne_self, false_or] at this
    rw [this, Nat.add_zero]

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inl.false
n i : ℕ
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit i = (false.toNat * 2 ^ i).testBit i

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inl.true
n i : ℕ
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit i = (true.toNat * 2 ^ i).testBit i

Tactic:
simp [h]

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

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
a : α
h : filterMap id l = [a]
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
filterMap_eq_cons_iff

Goal state after:
case mp
α : Type u_1
l : List (Option α)
a : α
h : ∃ l₁ a_1 l₂, l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : Option α), x ∈ l₁ → id x = none) ∧ id a_1 = some a ∧ filterMap id l₂ = []
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m : PosNum
⊢ ∀ (n : PosNum), (m.cmp n).swap = n.cmp m

Tactic:
induction m with | one => ?_ | bit1 m IH => ?_ | bit0 m IH => ?_ <;>
    intro n <;> obtain - | n | n := n <;> unfold cmp <;>
      try { rfl } <;> rw [← IH] <;> cases cmp m n

Goal state after:
case bit1.bit0.lt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.lt Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.lt.swap Ordering.lt Ordering.lt Ordering.gt

case bit1.bit0.eq
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.eq Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.eq.swap Ordering.lt Ordering.lt Ordering.gt

case bit1.bit0.gt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.gt Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.gt.swap Ordering.lt Ordering.lt Ordering.gt

case bit0.bit1.lt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.lt Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.lt.swap Ordering.lt Ordering.gt Ordering.gt

case bit0.bit1.eq
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.eq Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.eq.swap Ordering.lt Ordering.gt Ordering.gt

case bit0.bit1.gt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.gt Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.gt.swap Ordering.lt Ordering.gt Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
h : Ordering.casesOn Ordering.lt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
h : Ordering.casesOn Ordering.eq (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : Num
h : Ordering.casesOn Ordering.lt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : Num
h : Ordering.casesOn Ordering.eq (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
n : PosNum
⊢ 1 ≤ ↑n

Tactic:
rw [← cast_to_nat, ← Nat.cast_one, Nat.cast_le (α := α)]; apply to_nat_pos

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : n.pred' = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = (↑n).pred

Tactic:
rw [← pred'_to_nat, e]
    rfl

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_2.succ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
c : ℕ
this : true = (ofNat (Option ℕ) (c + 1)).isSome
⊢ b = (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b

Tactic:
rw [← Option.some_inj, eq_comm]

Goal state after:
case refine_2.succ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
c : ℕ
this : true = (ofNat (Option ℕ) (c + 1)).isSome
⊢ some (c + 1).pred = some b ↔ ofNat (Option ℕ) (c + 1) = some b
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail.inr.refl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
e₂ : σ₂
ce : Reaches f₂ b✝ e₂
ee : tr e₁ e₂
ae : Reaches f₁ a₁ e₁
cd' : c✝ ∈ f₂ b✝
de : ReflTransGen (fun a b ↦ b ∈ f₂ a) c✝ e₂
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
exact ⟨_, _, de, ee, ae⟩

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
h₂ : SupportsStmt S (M l₁)
⊢ (stepAux (M l₁) v T).l ∈ Finset.insertNone S

Tactic:
revert h₂

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
⊢ SupportsStmt S (M l₁) → (stepAux (M l₁) v T).l ∈ Finset.insertNone S
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: 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₁ : Λ
v : σ
T : (k : K) → List (Γ k)
h₂ : SupportsStmt S (M l₁)
⊢ (stepAux (M l₁) v T).l ∈ Finset.insertNone S

Tactic:
revert h₂

Goal state after:
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₁ : Λ
v : σ
T : (k : K) → List (Γ k)
⊢ SupportsStmt S (M l₁) → (stepAux (M l₁) v T).l ∈ Finset.insertNone S
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
⊢ (hd :: tl).reverse[tl.length]? = some hd

Tactic:
rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length]

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

Goal state before:
pp: case load
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
a : σ → σ
q✝ : TM2.Stmt Γ Λ σ
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = 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 L))) b
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.load a q✝) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (TM2.Stmt.load a q✝)) v (Tape.mk' ∅ (addBottom L))) b

Tactic:
| load a _ IH =>

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

Goal state before:
pp: case pos
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 (stepRet k v'.tail)
⊢ ∃ v₂ ∈ pure v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
refine ⟨_, Part.mem_some _, ?_⟩
        rw [reaches_eval]
        · exact h
        exact ReflTransGen.single rfl

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

Goal state before:
pp: case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step ?m.617
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)

pp: case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ Reaches step (Cfg.ret k v') ?m.617

pp: f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ Cfg

Tactic:
swap

Goal state after:
case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ Reaches step (Cfg.ret k v') ?m.617

case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step ?m.617
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)

f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

pp: p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = ([], o, L₂)
⊢ [].reverseAux (S k₂) = update S k₁ L₂ k₂

Tactic:
swap

Goal state after:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = ([], o, L₂)
⊢ [].reverseAux (S k₂) = update S k₁ L₂ k₂

case nil
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = ([], o, L₂)
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
    { l := some q, var := o, stk := update S k₁ L₂ }
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.61 = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

pp: case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v✝ k) v) ?m.61

pp: f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg

Tactic:
swap

Goal state after:
case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v✝ k) v) ?m.61

case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.61 = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.171 = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

pp: case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) ?m.171

pp: f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg

Tactic:
swap

Goal state after:
case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) ?m.171

case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.171 = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons₁
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₁ fs as k) v) = Cfg.halt <$> (Cont.cons₁ fs as k).eval v

Tactic:
rw [Cont.eval, stepRet, code_is_ok]

Goal state after:
case cons₁
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v_1 ← fs.eval as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    Cfg.halt <$>
      (fun v ↦ do
          let ns ← fs.eval as
          k.eval (v.headI :: ns))
        v
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.89 = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') ?m.89

pp: fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg

Tactic:
swap

Goal state after:
case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') ?m.89

case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.89 = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet (Cont.comp f k) v) = Cfg.halt <$> (Cont.comp f k).eval v

Tactic:
rw [Cont.eval, stepRet, code_is_ok]

Goal state after:
case comp
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v ← f.eval v
      eval step (Cfg.ret k v)) =
    Cfg.halt <$> (fun v ↦ f.eval v >>= k.eval) v
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.167 = do
    let a ← k.eval v'
    pure (Cfg.halt a)

pp: case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret k v') ?m.167

pp: f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg

Tactic:
swap

Goal state after:
case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret k v') ?m.167

case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.167 = do
    let a ← k.eval v'
    pure (Cfg.halt a)

f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_5
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
x✝¹ : TM2.SupportsStmt S TM2.Stmt.halt
x✝ : ∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
exact ⟨trivial, fun _ ↦ False.elim⟩

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝³ : TopologicalSpace A
inst✝² : ExtremallyDisconnected A
inst✝¹ : CompactSpace A
inst✝ : T2Space A
⊢ Projective A

Tactic:
intro B

Goal state after:
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : ExtremallyDisconnected A
inst✝¹ : CompactSpace A
inst✝ : T2Space A
B : Type u
⊢ ∀ {Z : Type u} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace Z] [CompactSpace B] [T2Space B] [CompactSpace Z]
    [T2Space Z] {f : A → Z} {g : B → Z}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
⊢ PreirreducibleSpace X

Tactic:
apply (preirreducibleSpace_iff_open_dense X).mpr (fun s hs sn ↦ ?_)
  apply dense_iff_closure_eq.mpr
  cases preconnectedSpace_iff_clopen.mp h' (closure s) ⟨isClosed_closure, h.open_closure s hs⟩
  · simp_all
  · assumption

Goal state after:
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
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
t : ↑X.toTop
⊢ (g ∘ ⇑(ConcreteCategory.hom h)) t = f t

Tactic:
apply_fun (fun e => e t) at hh

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
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h : X ⟶ A'
t : ↑X.toTop
hh : (ConcreteCategory.hom (h ≫ g')) t = (ConcreteCategory.hom f') t
⊢ (g ∘ ⇑(ConcreteCategory.hom h)) t = f t
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
⊢ ∀ {E X_1 : CompHaus} (f : toCompHaus.obj X ⟶ X_1) (e : E ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f

Tactic:
intro B

Goal state after:
X : Stonean
B : CompHaus
⊢ ∀ {X_1 : CompHaus} (f : toCompHaus.obj X ⟶ X_1) (e : B ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
⊢ ∀ {E X_1 : Profinite} (f : toProfinite.obj X ⟶ X_1) (e : E ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f

Tactic:
intro B

Goal state after:
X : Stonean
B : Profinite
⊢ ∀ {X_1 : Profinite} (f : toProfinite.obj X ⟶ X_1) (e : B ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
⊢ ∀ {E X_1 : Stonean} (f : X ⟶ X_1) (e : E ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f

Tactic:
intro B

Goal state after:
X B : Stonean
⊢ ∀ {X_1 : Stonean} (f : X ⟶ X_1) (e : B ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
· refine
      TransGen.trans
        (move_ok (by decide)
          (splitAtPred_eq _ _ (trNat a) (some Γ'.cons) (trList L₂ ++ Γ'.consₗ :: L₃)
            (trNat_natEnd _) ⟨rfl, by simp⟩))
        (TransGen.head rfl (TransGen.head rfl ?_))
    simp only [TM2.step, Option.mem_def, trList, List.append_assoc,
      List.cons_append, elim_update_stack, elim_rev, elim_update_rev, Function.update_self,
      List.headI_cons]
    refine
      TransGen.trans
        (clear_ok
          (splitAtPred_eq _ _ (trList L₂) (some Γ'.consₗ) L₃
            (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)) ⟨rfl, by simp⟩))
        ?_
    convert! unrev_ok using 2
    simp [List.reverseAux_eq]

Goal state after: