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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ 1 / 2 * f u ≤ 1 / 2 * (c₂ * f x)

Tactic:
gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:

Tactic:
_ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u - 1 / 2 * f u := by
                rw [sub_eq_add_neg]
                gcongr
                rwa [← neg_mul, ← neg_div]
           _ = 1 / 2 * f u := by ring
           _ ≤ 1 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = c₂ / 3 * (3 / 2 * f x) := by ring
           _ ≤ c₂ / 3 * (f x + g x) := by gcongr

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := ⋯
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
i : α
a✝ : i ∈ univ
⊢ sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n

Tactic:
· exact h_sumTransform i

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

Goal state before:
pp: m k : ℕ
⊢ 2 * ((m + 1) * 2 ^ k) = (m + 1) * 2 ^ (k + 1)

Tactic:
Nat.mul_left_comm,

Goal state after:
m k : ℕ
⊢ (m + 1) * (2 * 2 ^ k) = (m + 1) * 2 ^ (k + 1)
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) → x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
rintro ⟨s, hs, h | h⟩
    · left; tauto
    · right; tauto

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

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit1.cmp b.bit1) (↑a.bit1 < ↑b.bit1) (a.bit1 = b.bit1) (↑b.bit1 < ↑a.bit1)

Tactic:
by
    dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact Nat.succ_lt_succ (Nat.add_lt_add this this)
    · rw [this]
    · exact Nat.succ_lt_succ (Nat.add_lt_add this this)

Goal state after:
Module: Mathlib.Computability.Halting

Goal state before:
pp: C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c ↦ c.eval ∈ C
h : Computable fun a ↦ decide ((fun c ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun b ↦ if c.eval ∈ C then g b else f b
⊢ g ∈ C

Tactic:
by_cases H : eval c ∈ C

Goal state after:
case pos
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c ↦ c.eval ∈ C
h : Computable fun a ↦ decide ((fun c ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun b ↦ if c.eval ∈ C then g b else f b
H : c.eval ∈ C
⊢ g ∈ C

case neg
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c ↦ c.eval ∈ C
h : Computable fun a ↦ decide ((fun c ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun b ↦ if c.eval ∈ C then g b else f b
H : c.eval ∉ C
⊢ g ∈ C
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
⊢ n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
by rw [← cmp_swap]; cases cmp m n <;> decide

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

Goal state before:
pp: m n : Num
⊢ n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
by rw [← cmp_swap]; cases cmp m n <;> decide

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: case inl.inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
h' : (k a).get this ∈ g a
⊢ (k a).get this = x

pp: case inr.inl
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : (k a).get this ∈ f a
⊢ (k a).get this = x

pp: case inr.inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : (k a).get this ∈ g a
⊢ (k a).get this = x

Tactic:
· exact (H _ _ h _ h').symm

Goal state after:
case inr.inl
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : (k a).get this ∈ f a
⊢ (k a).get this = x

case inr.inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : (k a).get this ∈ g a
⊢ (k a).get this = x
Module: Mathlib.Computability.StateTransition

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

pp: case inr
σ₁ : 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₁
ab : TransGen (fun a b ↦ b ∈ f₁ a) a₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
· exact ⟨_, aa, ReflTransGen.refl⟩

Goal state after:
case inr
σ₁ : 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₁
ab : TransGen (fun a b ↦ b ∈ f₁ a) a₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail.inl
σ₁ : 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₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
⊢ (match f₁ e₁ with
    | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ b✝ b₂
    | none => f₂ b✝ = none) →
    ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
rcases eg : f₁ e₁ with - | g₁

Goal state after:
case tail.inl.none
σ₁ : 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₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
eg : f₁ e₁ = none
⊢ (match none with
    | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ b✝ b₂
    | none => f₂ b✝ = none) →
    ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

case tail.inl.some
σ₁ : 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₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
⊢ (match some g₁ with
    | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ b✝ b₂
    | none => f₂ b✝ = none) →
    ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
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₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab : b₂ ∈ eval f₂ a₂
⊢ ∃ b₁, tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁

Tactic:
by
  obtain ⟨ab, b0⟩ := mem_eval.1 ab
  rcases tr_reaches_rev H aa ab with ⟨c₁, c₂, bc, cc, ac⟩
  cases (reflTransGen_iff_eq (Option.eq_none_iff_forall_not_mem.1 b0)).1 bc
  refine ⟨_, cc, mem_eval.2 ⟨ac, ?_⟩⟩
  have := H cc
  rcases hfc : f₁ c₁ with - | d₁
  · rfl
  rw [hfc] at this
  rcases this with ⟨d₂, _, bd⟩
  rcases TransGen.head'_iff.1 bd with ⟨e, h, _⟩
  cases b0.symm.trans h

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ (char a).rmatch [head✝] = true ↔ [head✝] = [a]

Tactic:
rw [rmatch, deriv, List.singleton_inj]

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ (if a = head✝ then 1 else 0).rmatch [] = true ↔ head✝ = a
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
x : List α
⊢ (char a).rmatch (head✝ :: x) = true ↔ head✝ :: x = [a]

Tactic:
rcases x with - | ⟨head, tail⟩
    · rw [rmatch, deriv, List.singleton_inj]
      split <;> tauto
    · rw [rmatch, rmatch, deriv, cons.injEq]
      split
      · simp_rw [deriv_one, zero_rmatch, reduceCtorEq, and_false]
      · simp_rw [deriv_zero, zero_rmatch, reduceCtorEq, and_false]

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

Goal state before:
pp: case right.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
q' : Option (TM1.Stmt Γ Λ σ)
v' : σ
h₁ : ((q', v'), s) ∈ tr M (some q, v) a
h₂ : (some q, v).1 ∈ TM1.stmts M S ∧ (some q, v).2 ∈ Finset.univ
⊢ (q', v').1 ∈ TM1.stmts M S ∧ (q', v').2 ∈ Finset.univ

Tactic:
simp only [Finset.mem_univ, and_true] at h₂ ⊢

Goal state after:
case right.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
q' : Option (TM1.Stmt Γ Λ σ)
v' : σ
h₁ : ((q', v'), s) ∈ tr M (some q, v) a
h₂ : some q ∈ TM1.stmts M S
⊢ q' ∈ TM1.stmts M S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some.some.load
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
b : Γ → σ → σ
q : TM1.Stmt Γ Λ σ
IH :
  ∀ (v : σ),
    some q ∈ TM1.stmts M S →
      some (trAux M a q v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.load b q) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.load b q) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.load b q)
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
| load b q IH =>

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

Goal state before:
pp: case rfind.mpr.zero
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
w : List ℕ
hm : ∀ {m : ℕ}, m < 0 → ¬f (m ::ᵥ v) = 0
this :
  w ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: ↑v)
⊢ w ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: ↑v)

Tactic:
exact this

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: case fst
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
z : ↑Z.toTop
hfst : (ConcreteCategory.hom (a ≫ fst f g)) z = (ConcreteCategory.hom (b ≫ fst f g)) z
hsnd : (ConcreteCategory.hom (a ≫ snd f g)) z = (ConcreteCategory.hom (b ≫ snd f g)) z
⊢ (↑((ConcreteCategory.hom a) z)).1 = (↑((ConcreteCategory.hom b) z)).1

Tactic:
exact hfst

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 _, ?_⟩

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)
⊢ x ∈ eval step (Cfg.ret k v'.tail)
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case mp
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
⊢ U ∈ 𝓝 x → ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
intro hU

Goal state after:
case mp
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
simp at h₃

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

Goal state before:
pp: case cons
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a) (TM2.stepAux (tr (Λ'.move p k₁ k₂ q)) s S)
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Tactic:
rw [tr]

Goal state after:
case cons
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (pop' k₁ (branch (fun s ↦ s.elim true p) (goto fun x ↦ q) (push' k₂ (goto fun x ↦ Λ'.move p k₁ k₂ q))))
      s S)
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mp
X Y : Profinite
f : X ⟶ Y
⊢ (∃ b, ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ b) → ¬Epi f

Tactic:
rintro ⟨y, hy⟩ hf

Goal state after:
case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
⊢ False
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 (tr (Λ'.push k₁ id (Λ'.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₂) }

Tactic:
rw [tr]

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

Goal state before:
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 (tr (Λ'.push k₁ id (Λ'.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:
rw [tr]

Goal state after:
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
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
⊢ ReflTransGen (fun a b ↦ b ∈ TM2.step tr a) (TM2.stepAux (tr (Λ'.clear p k q)) s S)
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
rw [tr]

Goal state after:
case nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
⊢ ReflTransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (pop' k (branch (fun s ↦ s.elim true p) (goto fun x ↦ q) (goto fun x ↦ Λ'.clear p k q))) s S)
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a) (TM2.stepAux (tr (Λ'.clear p k q)) s S)
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
rw [tr]

Goal state after:
case cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (pop' k (branch (fun s ↦ s.elim true p) (goto fun x ↦ q) (goto fun x ↦ Λ'.clear p k q))) s S)
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a) (TM2.stepAux (tr q.copy) s (elim a (x :: b) c d))
    { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }

Tactic:
rw [tr]

Goal state after:
case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (pop' rev (branch Option.isSome (push' main (push' stack (goto fun x ↦ q.copy))) (goto fun x ↦ q))) s
      (elim a (x :: b) c d))
    { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }