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

Goal state before:
pp: f : ℝ → ℝ
p : ℤ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x ^ p

Tactic:
simp_rw [← rpow_intCast]

Goal state after:
f : ℝ → ℝ
p : ℤ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x ^ ↑p
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ log x + log b = log (b * x)

Tactic:
by rw [← Real.log_mul (by positivity) (by positivity), mul_comm]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.rfind'.some
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
x : ℕ
⊢ Nat.rec (some (unpair n).2)
      (fun n_1 n_ih ↦
        lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      x =
    if x = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))

Tactic:
cases x

Goal state after:
case succ.rfind'.some.zero
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ Nat.rec (some (unpair n).2)
      (fun n_1 n_ih ↦
        lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      0 =
    if 0 = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))

case succ.rfind'.some.succ
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
n✝ : ℕ
⊢ Nat.rec (some (unpair n).2)
      (fun n_1 n_ih ↦
        lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
          (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
      (n✝ + 1) =
    if n✝ + 1 = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
⊢ ↑m < ↑n → ↑m + ↑m + 1 + 1 ≤ ↑n + ↑n

Tactic:
intro h

Goal state after:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m + ↑m + 1 + 1 ≤ ↑n + ↑n
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) → ∃ n, l = replicate n none

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
l : List (Option α)
h : ∀ (a : Option α), a ∈ l → id a = none
⊢ ∃ n, l = replicate n none
Module: Mathlib.Data.List.ReduceOption

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

Tactic:
intro h

Goal state after:
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
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] → ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : l.reduceOption = l' ++ [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
x : Option α
⊢ [x].reduceOption = x.toList

Tactic:
cases x

Goal state after:
case none
α : Type u_1
⊢ [none].reduceOption = none.toList

case some
α : Type u_1
val✝ : α
⊢ [some val✝].reduceOption = (some val✝).toList
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case nil
α : Type u_1
x : Option α
⊢ ([].concat x).reduceOption = [].reduceOption ++ x.toList

Tactic:
cases x

Goal state after:
case nil.none
α : Type u_1
⊢ ([].concat none).reduceOption = [].reduceOption ++ none.toList

case nil.some
α : Type u_1
val✝ : α
⊢ ([].concat (some val✝)).reduceOption = [].reduceOption ++ (some val✝).toList
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ 0 ≤ 1

Tactic:
by decide

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
by decide

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

Goal state before:
pp: n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ ↑zero
⊢ ¬1 ≤ ↑zero

Tactic:
by decide

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

Goal state before:
pp: p : PosNum
⊢ ↑p.pred' = (↑(pos p)).pred

Tactic:
PosNum.pred'_to_nat

Goal state after:
p : PosNum
⊢ (↑p).pred = (↑(pos p)).pred
Module: Mathlib.Computability.RE

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

Tactic:
intro h

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

Goal state before:
pp: σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab : Reaches₁ f₁ a₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
induction ab with
  | single ac =>
    have := H aa
    rwa [show f₁ a₁ = _ from ac] at this
  | @tail c₁ d₁ _ cd IH =>
    rcases IH with ⟨c₂, cc, ac₂⟩
    have := H cc
    rw [show f₁ c₁ = _ from cd] at this
    rcases this with ⟨d₂, dd, cd₂⟩
    exact ⟨_, dd, ac₂.trans cd₂⟩

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
x : α ⊕ β
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)

Tactic:
cases x

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
val✝ : α
⊢ (p ⊕' q) (Sum.inl val✝) ↔ r ((f ⊕' g) (Sum.inl val✝))

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
val✝ : β
⊢ (p ⊕' q) (Sum.inr val✝) ↔ r ((f ⊕' g) (Sum.inr val✝))
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (P.matchEpsilon && Q.matchEpsilon) = true → ∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
intro h

Goal state after:
case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ ∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
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 : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f)) (update S k (stWrite v (S k) (StAct.peek f)))

Tactic:
unfold stWrite

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f))
      (update S k
        (match StAct.peek f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => (S k).tail))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
intro h

Goal state after:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
⊢ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
a : α
⊢ colimit.ι (Discrete.functor X) { as := a } ≫ Sigma.desc π =
    colimit.ι (Discrete.functor X) { as := a } ≫ i.hom ≫ finiteCoproduct.desc X π

Tactic:
simp only [i, Discrete.functor_obj, colimit.ι_desc, Cofan.mk_ι_app,
      colimit.comp_coconePointUniqueUpToIso_hom_assoc]

Goal state after:
α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
a : α
⊢ π a = finiteCoproduct.ι X a ≫ finiteCoproduct.desc X π
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
⊢ x ∈ eval step (stepRet k v'.tail) → ∃ v₂ ∈ pure v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
intro h

Goal state after:
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₂)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case neg
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
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail) → ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
intro h

Goal state after:
case neg
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)
⊢ ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case branch.true
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
p : σ → Bool
q₁ 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
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 (bif true then TM2.stepAux q₁ v S else TM2.stepAux q₂ v S) b ∧
      Reaches (TM1.step (tr M))
        (bif true then TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))
        else TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L)))
        b

Tactic:
exact IH₁ _ hT

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

Goal state before:
pp: case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
p : σ → Bool
q₁ 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
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.branch p q₁ q₂) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (TM2.Stmt.branch p q₁ q₂)) v (Tape.mk' ∅ (addBottom L))) b

Tactic:
unfold TM2.stepAux trNormal TM1.stepAux
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/12129): additional beta reduction needed
    beta_reduce
    cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]

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

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

Tactic:
cases x

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

case rev
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' rev = elim a' b c d rev

case aux
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' aux = elim a' b c d aux

case stack
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' stack = elim a' b c d stack
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
cases x

Goal state after:
case main
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' main = elim a b' c d main

case rev
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' rev = elim a b' c d rev

case aux
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' aux = elim a b' c d aux

case stack
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' stack = elim a b' c d stack
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
cases x

Goal state after:
case main
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' main = elim a b c' d main

case rev
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' rev = elim a b c' d rev

case aux
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' aux = elim a b c' d aux

case stack
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' stack = elim a b c' d stack
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
cases x

Goal state after:
case main
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' main = elim a b c d' main

case rev
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' rev = elim a b c d' rev

case aux
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' aux = elim a b c d' aux

case stack
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' stack = elim a b c d' stack
Module: Mathlib.Topology.Separation.Profinite

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

Tactic:
intro h

Goal state after:
case mp
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
h : TotallyDisconnectedSpace H
⊢ TotallySeparatedSpace H
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
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ TM1.init (trInit k L) =
    { l := Option.map normal (some default), var := default,
      Tape := Tape.mk' ∅ (addBottom (ListBlank.mk (List.map (fun a ↦ update default k (some a)) L.reverse))) }

Tactic:
· rw [trInit, TM1.init]
    congr <;> cases L.reverse <;> try rfl
    simp only [List.map_map, List.tail_cons, List.map]
    rfl

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

Goal state before:
pp: q : Λ'
s : Option Γ'
S : K' → List Γ'
⊢ rev ≠ main

Tactic:
by decide

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

Goal state before:
pp: a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l
⊢ x ≠ Γ'.consₗ

Tactic:
obtain h | rfl | h := h

Goal state after:
case inl
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a
⊢ x ≠ Γ'.consₗ

case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ

case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X Y : Stonean
f : X ⟶ Y
⊢ Epi f → ∀ (b : ↑Y.toTop), ∃ a, (ConcreteCategory.hom f) a = b

Tactic:
intro h

Goal state after:
X Y : Stonean
f : X ⟶ Y
h : Epi f
⊢ ∀ (b : ↑Y.toTop), ∃ a, (ConcreteCategory.hom f) a = b
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ main ≠ rev

Tactic:
by decide

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

Goal state before:
pp: q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ stack ≠ rev

Tactic:
by decide

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

Goal state before:
pp: q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ stack ≠ rev

Tactic:
by decide

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: case mp
X : CompHaus
⊢ Projective X → ExtremallyDisconnected ↑X.toTop

Tactic:
intro h

Goal state after:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected ↑X.toTop