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

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
hf' : 0 ≤ᶠ[atTop] f
hg' : 0 ≤ᶠ[atTop] g
b : ℝ
⊢ b ∈ Set.Ioo 0 1 →
    ∃ c₁ > 0,
      ∃ c₂ > 0,
        ∀ᶠ (x : ℝ) in atTop,
          ∀ u ∈ Set.Icc (b * x) x,
            (fun x ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun x ↦ f x + g x) x) (c₂ * (fun x ↦ f x + g x) x)

Tactic:
hb

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
hf' : 0 ≤ᶠ[atTop] f
hg' : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun x ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun x ↦ f x + g x) x) (c₂ * (fun x ↦ f x + g x) x)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g ↑n ≤ sumTransform (p a b) g (r i n) n

Tactic:
obtain ⟨c₂, hc₂_mem, hc₂⟩ := R.g_grows_poly.eventually_atTop_ge_nat hc₁_mem

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g ↑n ≤ sumTransform (p a b) g (r i n) n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hfg : g =o[atTop] f
b : ℝ
⊢ b ∈ Set.Ioo 0 1 →
    ∃ c₁ > 0,
      ∃ c₂ > 0,
        ∀ᶠ (x : ℝ) in atTop,
          ∀ u ∈ Set.Icc (b * x) x,
            (fun x ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun x ↦ f x + g x) x) (c₂ * (fun x ↦ f x + g x) x)

Tactic:
hb

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hfg : g =o[atTop] f
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun x ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun x ↦ f x + g x) x) (c₂ * (fun x ↦ f x + g x) x)
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' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) 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
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, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ 1 - C * c₁ * (1 - ε ↑n) ≤ 0

Tactic:
rw [sub_nonpos]

Goal state after:
case h₂
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) 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
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, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ 1 ≤ C * c₁ * (1 - ε ↑n)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case bc.a
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
⊢ - -‖g x‖ ≤ -(1 / 2 * f x)

Tactic:
rwa [neg_neg, ← neg_mul, ← neg_div]

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

Goal state before:
pp: case h₂
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
⊢ - -‖g u‖ ≤ -(1 / 2 * f u)

Tactic:
rwa [neg_neg, ← neg_mul, ← neg_div]

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
x✝ : List α
h : x✝ ∈ []
⊢ x✝ ∈ l

Tactic:
by contradiction

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

Goal state before:
pp: case inr
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf : GrowsPolynomially fun x ↦ |f x|
b : ℝ
⊢ b ∈ Set.Ioo 0 1 →
    ∃ c₁ > 0,
      ∃ c₂ > 0,
        ∀ᶠ (x : ℝ) in atTop,
          ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|⁻¹) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|⁻¹) x) (c₂ * (fun x ↦ |f x|⁻¹) x)

Tactic:
hb

Goal state after:
case inr
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|⁻¹) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|⁻¹) x) (c₂ * (fun x ↦ |f x|⁻¹) x)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
⊢ b ∈ Set.Ioo 0 1 →
    ∃ c₁ > 0,
      ∃ c₂ > 0,
        ∀ᶠ (x : ℝ) in atTop,
          ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun x ↦ f x ^ p) x) (c₂ * (fun x ↦ f x ^ p) x)

Tactic:
hb

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun x ↦ f x ^ p) x) (c₂ * (fun x ↦ f x ^ p) x)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case pos
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, (bit b 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b 0).testBit j = false

Tactic:
show b = true by
        revert h
        cases b <;> simp

Goal state after:
case pos
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, (bit true 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit true 0).testBit j = false
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n m k : ℕ
⊢ n &&& m &&& k = n &&& (m &&& k)

Tactic:
bitwise_assoc_tac

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

Goal state before:
pp: n m k : ℕ
⊢ n ||| m ||| k = n ||| (m ||| k)

Tactic:
bitwise_assoc_tac

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

Goal state before:
pp: b : ℝ
⊢ b ∈ Set.Ioo 0 1 →
    ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (c₁ * log x) (c₂ * log x)

Tactic:
hb

Goal state after:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (c₁ * log x) (c₂ * log x)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
⊢ b ∈ Set.Ioo 0 1 →
    ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
hb

Goal state after:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: a : Code × ℕ
⊢ (rfindOpt fun b ↦
      evaln (((a, b).2, (a, b).1.1), (a, b).1.2).1.1 (((a, b).2, (a, b).1.1), (a, b).1.2).1.2
        (((a, b).2, (a, b).1.1), (a, b).1.2).2) =
    a.1.eval a.2

Tactic:
simp [eval_eq_rfindOpt]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
⊢ M.IsPath s t [a] → t ∈ M.step s a

Tactic:
rintro (_ | ⟨_, _, _, _, _, _, ⟨⟩⟩)

Goal state after:
case cons.nil
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
a✝ : t ∈ M.step s a
⊢ t ∈ M.step s a
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate 0 none)
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
List.replicate_zero

Goal state after:
case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ []
⊢ s₂ ∈ M.εClosure {s₁}
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h✝ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ (List.replicate n none).reduceOption = [] ∧ M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
rw [List.reduceOption_replicate_none]

Goal state after:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h✝ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ [] = [] ∧ M.IsPath s₁ s₂ (List.replicate n none)
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_2
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)
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
· have := Nat.rfind_spec h
        simp only [Part.coe_some, Part.mem_some_iff] at this
        revert this; rcases f (a ::ᵥ v) with - | c <;> intro this
        · cases this
        rw [← Option.some_inj, eq_comm]
        rfl

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

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

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

Goal state before:
pp: case inr.inr
Γ : Type ?u.5
inst✝ : Inhabited Γ
l✝ : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
h₂ : n < (l ++ List.replicate i default).length
⊢ default = (l ++ List.replicate i default).getI n

Tactic:
List.getI_eq_getElem _ h₂,

Goal state after:
case inr.inr
Γ : Type ?u.5
inst✝ : Inhabited Γ
l✝ : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
h₂ : n < (l ++ List.replicate i default).length
⊢ default = (l ++ List.replicate i default)[n]
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case push
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
⊢ { f := fun a ↦ a k', map_pt' := ⋯ }.f (if i = (S k).length then update (L.nth i) k (some (f v)) else L.nth i) =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i

Tactic:
PointedMap.mk_val

Goal state after:
case push
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
⊢ (if i = (S k).length then update (L.nth i) k (some (f v)) else L.nth i) k' =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.prec.succ.zero
n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ :
  (cf.prec cg).eval (n :: (↑v).tail) =
    pure (pure (Nat.rec (f (n ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (n ::ᵥ v.tail).tail)) (n ::ᵥ v.tail).head))
a : ℕ
e : a + 0 = n
⊢ n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
    PFun.fix
      (fun v ↦
        (cg.eval (v.headI :: v.tail.tail)).bind fun x ↦
          Part.some
            (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
            else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
      (a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)

Tactic:
refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)

Goal state after:
case prim.prec.succ.zero
n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ :
  (cf.prec cg).eval (n :: (↑v).tail) =
    pure (pure (Nat.rec (f (n ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (n ::ᵥ v.tail).tail)) (n ::ᵥ v.tail).head))
a : ℕ
e : a + 0 = n
⊢ ((cg.eval
          ((a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI ::
            (a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.tail)).bind
      fun x ↦
      Part.some
        (if (a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.headI = 0 then
          Sum.inl
            ((a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.succ ::
              (a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.headI.pred ::
                x.headI ::
                  (a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.tail.tail)
        else
          Sum.inr
            ((a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.succ ::
              (a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.headI.pred ::
                x.headI ::
                  (a :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).tail.tail.tail))) =
    Part.some
      (Sum.inl
        (n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail))
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case pop.cons
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
k' : K
i : ℕ
⊢ { f := fun a ↦ a k', map_pt' := ⋯ }.f (if i = tl.length then update (L.nth i) k none else L.nth i) =
    (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i

Tactic:
PointedMap.mk_val

Goal state after:
case pop.cons
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
k' : K
i : ℕ
⊢ (if i = tl.length then update (L.nth i) k none else L.nth i) k' =
    (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacksOfInclusions P
⊢ ∀ {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)

Tactic:
intro X

Goal state after:
P : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacksOfInclusions P
X : CompHausLike P
⊢ ∀ {Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (a✝.then k')) a✝¹ = (stepNormal a✝² (Cont.cons₂ v a✝) a✝¹).then k'

Tactic:
rw [← stepNormal_then]

Goal state after:
case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (a✝.then k')) a✝¹ = stepNormal a✝² ((Cont.cons₂ v a✝).then k') a✝¹
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝¹ (a✝.then k') v = (stepNormal a✝¹ a✝ v).then k'

Tactic:
rw [← stepNormal_then]

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

Goal state before:
pp: case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : ¬v.headI = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail = (stepNormal a✝¹ (Cont.fix a✝¹ a✝) v.tail).then k'

Tactic:
rw [← stepNormal_then]

Goal state after:
case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : ¬v.headI = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail = stepNormal a✝¹ ((Cont.fix a✝¹ a✝).then k') v.tail
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ ∀ {X Y Z : CompHausLike P} (f : X ⟶ Y) (g : Z ⟶ Y) [EffectiveEpi g], ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f

Tactic:
intro X

Goal state after:
P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X : CompHausLike P
⊢ ∀ {Y Z : CompHausLike P} (f : X ⟶ Y) (g : Z ⟶ Y) [EffectiveEpi g], ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f
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)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
⊢ (Option.map (fun a ↦ { f := fun a ↦ a k', map_pt' := ⋯ }.f (update default k (some a))) L.reverse[i]?).getD default =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i

Tactic:
PointedMap.mk_val

Goal state after:
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)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
⊢ (Option.map (fun a ↦ update default k (some a) k') L.reverse[i]?).getD default =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he✝¹ : v'.tail ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he✝ : v'.tail ∈ f.fix.eval v
he : Sum.inl v'.tail ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
⊢ x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)

Tactic:
if_pos h

Goal state after:
case pos.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he✝¹ : v'.tail ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he✝ : v'.tail ∈ f.fix.eval v
he : Sum.inl v'.tail ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
⊢ x ∈ eval step (stepRet k v'.tail)
Module: Mathlib.Topology.Category.CompHaus.Projective

Goal state before:
pp: X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Epi g
⊢ ∃ f', f' ≫ g = f

Tactic:
rw [epi_iff_surjective] at hg
    obtain ⟨g', hg'⟩ := hg.hasRightInverse
    let t : X → Y := g' ∘ f ∘ (pure : X → Ultrafilter X)
    let h : Ultrafilter X → Y := Ultrafilter.extend t
    have hh : Continuous h := continuous_ultrafilter_extend _
    use CompHausLike.ofHom _ ⟨h, hh⟩
    apply ConcreteCategory.coe_ext
    have : g.hom ∘ g' = id := hg'.comp_eq_id
    convert!
      denseRange_pure.equalizer (g.hom.hom.continuous.comp hh) f.hom.hom.continuous
        _
          -- This used to be `rw`, but we need `rw; rfl` after https://github.com/leanprover/lean4/pull/2644

    -- This used to be `rw`, but we need `rw; rfl` after https://github.com/leanprover/lean4/pull/2644
    rw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp]
    rfl

Goal state after: