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

Goal state before:
pp: m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack (m + 1) (n₂ + 1)

Tactic:
ack_succ_succ

Goal state after:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 < ack (m + 1) (n + 1)

Tactic:
ack_succ_succ

Goal state after:
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 < ack m (ack (m + 1) n)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
h : 0 < m + 1
⊢ ack 0 (n + 1) < ack (m + 1) (n + 1)

Tactic:
by
    rw [ack_zero, ack_succ_succ]
    calc
      n + 1 + 1 ≤ m + (m + 1 + n + 1) := by lia
      _ ≤ m + ack (m + 1) n := by gcongr; exact add_add_one_le_ack ..
      _ < ack m (ack (m + 1) n) := add_lt_ack ..

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack (m₂ + 1) (n + 1)

Tactic:
ack_succ_succ

Goal state after:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack (m + 1) (n + 1)

Tactic:
ack_succ_succ

Goal state after:
case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack m (ack (m + 1) n)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 1 + 3) (n + 1)

Tactic:
ack_succ_succ

Goal state after:
m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case zero
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m : ℕ
⊢ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) 0 < ack (max a b + 9) (m + 0)

Tactic:
apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)

Goal state after:
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m : ℕ
⊢ max a b < max a b + 9
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (ack (max a b + 8).succ (m + n)) ≤ ack (max a b + 8).succ (m + n).succ

Tactic:
succ_eq_add_one,

Goal state after:
case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (ack (max a b + 8 + 1) (m + n)) ≤ ack (max a b + 8 + 1) (m + n).succ
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (ack (max a b + 8 + 1) (m + n)) ≤ ack (max a b + 8 + 1) (m + n).succ

Tactic:
succ_eq_add_one,

Goal state after:
case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (ack (max a b + 8 + 1) (m + n)) ≤ ack (max a b + 8 + 1) (m + n + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
hc : (⊤.deleteVerts Gmax.universalVerts).coe.oddComponents.ncard ≤ Gmax.universalVerts.ncard
⊢ False

Tactic:
obtain ⟨M, hM⟩ := Subgraph.IsPerfectMatching.exists_of_isClique_supp hvEven
      (by simpa [IsTutteViolator] using hc) h'

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
hc : (⊤.deleteVerts Gmax.universalVerts).coe.oddComponents.ncard ≤ Gmax.universalVerts.ncard
M : Gmax.Subgraph
hM : M.IsPerfectMatching
⊢ False
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (fun n ↦ ↑n * 1⁻¹) = fun n ↦ ↑n

Tactic:
ext; simp

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ z ^ (p - 1) / 1) = fun z ↦ z ^ (p - 1)

Tactic:
ext; simp

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

Goal state before:
pp: p : ℝ
⊢ GrowsPolynomially fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖

Tactic:
cases eq_or_ne p 0 with
  | inl hp => -- p = 0
    have h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖)
        =ᶠ[atTop] fun z => z⁻¹ / (log z ^ 2) := by
      filter_upwards [eventually_deriv_one_add_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos
      have : 0 ≤ x⁻¹ / (log x ^ 2) := by positivity
      simp only [neg_div, norm_neg, hp, Real.rpow_zero,
        one_mul, hx, Real.norm_of_nonneg this]
    refine GrowsPolynomially.congr_of_eventuallyEq h₁ ?_
    refine GrowsPolynomially.div (GrowsPolynomially.inv growsPolynomially_id)
      (GrowsPolynomially.pow 2 growsPolynomially_log ?_)
    filter_upwards [eventually_ge_atTop 1] with x hx using log_nonneg hx
  | inr hp => -- p ≠ 0
    refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p - 1))
      (isTheta_deriv_rpow_p_mul_one_add_smoothingFn hp) ?_
    filter_upwards [eventually_gt_atTop 0] with _ _
    positivity

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

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ ↑⌈-logb 2 (x / x₀)⌉₊ ≤ 1 + ↑⌊-logb 2 (x / x₀)⌋₊

Tactic:
by rw [add_comm]; exact_mod_cast Nat.ceil_le_floor_add_one _

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

Goal state before:
pp: α : 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₀ : ℕ
⊢ R.n₀ ≤ n₀ →
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ C₀,
          (∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)) → T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)

Tactic:
n₀_ge_Rn₀

Goal state after:
α : 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₀
⊢ ∃ C₀,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ C ≥ C₀,
        (∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)) → T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : 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 : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
⊢ R.n₀ ≤ n₀ →
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ C₀,
          (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) → (1 + ε ↑n) * asympBound g a b n ≤ C * T n

Tactic:
n₀_ge_Rn₀

Goal state after:
α : 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 : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
⊢ ∃ C₀,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ C ≥ C₀, (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) → (1 + ε ↑n) * asympBound g a b n ≤ C * T n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n : Primrec Prod.snd
⊢ Primrec fun p ↦
    (fun a n ↦
        Nat.casesOn (ofNat (ℕ × Code) a.length).1 Option.none fun k' ↦
          Code.recOn (ofNat (ℕ × Code) a.length).2 (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2)
            (fun cf cg x x_1 ↦ do
              let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) n
              let y ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
              some (Nat.pair x y))
            (fun cf cg x x_1 ↦ do
              let x ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
              lup a ((ofNat (ℕ × Code) a.length).1, cf) x)
            (fun cf cg x x_1 ↦
              have z := (unpair n).1;
              Nat.casesOn (unpair n).2 (lup a ((ofNat (ℕ × Code) a.length).1, cf) z) fun y ↦ do
                let i ← lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z y)
                lup a ((ofNat (ℕ × Code) a.length).1, cg) (Nat.pair z (Nat.pair y i)))
            fun cf x ↦
            have z := (unpair n).1;
            have m := (unpair n).2;
            do
            let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) (Nat.pair z m)
            Nat.casesOn x (some m) fun x ↦ lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z (m + 1)))
      p.1 p.2

Tactic:
refine Primrec.nat_casesOn k (_root_.Primrec.const Option.none) (?_ : Primrec _)

Goal state after:
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n : Primrec Prod.snd
⊢ Primrec fun p ↦
    (fun p k' ↦
        Code.recOn (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ) (some (unpair p.2).1) (some (unpair p.2).2)
          (fun cf cg x x_1 ↦ do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
            let y ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            some (Nat.pair x y))
          (fun cf cg x x_1 ↦ do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
          (fun cf cg x x_1 ↦
            have z := (unpair p.2).1;
            Nat.casesOn (unpair p.2).2 (lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun y ↦ do
              let i ← lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
              lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
          fun cf x ↦
          have z := (unpair p.2).1;
          have m := (unpair p.2).2;
          do
          let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
          Nat.casesOn x (some m) fun x ↦ lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)))
      p.1 p.2
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Derives v w
p : List (Symbol T g.NT)
⊢ g.Derives (v ++ p) (w ++ p)

Tactic:
induction hvw with
  | refl => rfl
  | tail _ last ih => exact ih.trans_produces <| last.append_right p

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
⊢ g.reverse.language = g.language.reverse

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n

Tactic:
rw [decode_encodePosNum n]

Goal state after:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else ↑n) =
    Num.pos n
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, replicate l₁.length none ++ some a :: l₂ = replicate m none ++ some a :: replicate n none

Tactic:
hl₂

Goal state after:
case mp
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
w✝¹ w✝ : List (Option α)
h : l = w✝¹ ++ some a :: w✝
hl₁ : w✝¹.reduceOption = l'
hl₂ : w✝.reduceOption = []
⊢ l' ++ a :: w✝.reduceOption = l' ++ [a]

Tactic:
hl₂

Goal state after:
case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
w✝¹ w✝ : List (Option α)
h : l = w✝¹ ++ some a :: w✝
hl₁ : w✝¹.reduceOption = l'
hl₂ : w✝.reduceOption = []
⊢ l' ++ [a] = l' ++ [a]
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a

Tactic:
· exact cmp_to_nat_lemma this

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

Goal state before:
pp: case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a + 1 < ↑b + ↑b

pp: case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑a + ↑a + 1

pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a + 1

Tactic:
· exact cmp_to_nat_lemma this

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑a + ↑a + 1

case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a + 1
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l l₁ l₂ : List Γ
⊢ BlankExtends l l₁ → BlankExtends l l₂ → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

Tactic:
rintro ⟨i, rfl⟩ ⟨j, rfl⟩ h; use j - i
  simp only [List.length_append, Nat.add_le_add_iff_left, List.length_replicate] at h
  simp only [← List.replicate_add, Nat.add_sub_cancel' h, List.append_assoc]

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
⊢ ∀ {c c' : Cfg Γ Λ}, c' ∈ step M c → c.q ∈ S → c'.q ∈ S

Tactic:
intro ⟨q, T⟩

Goal state after:
Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
⊢ ∀ {c' : Cfg Γ Λ}, c' ∈ step M { q := q, Tape := T } → { q := q, Tape := T }.q ∈ S → c'.q ∈ S
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case e_a.succ
Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
n : ℕ
e : f default = List.replicate n default
i : ℕ
IH : List.flatMap f (List.replicate i default) = List.replicate (n * i) default
⊢ List.flatMap f (List.replicate (i + 1) default) = List.replicate (n * (i + 1)) default

Tactic:
simp only [IH, e, List.replicate_add, Nat.mul_succ, add_comm, List.replicate_succ,
      List.flatMap_cons]

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

Goal state before:
pp: Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ Tape Γ

Tactic:
constructor <;> apply default

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
⊢ q ∈ stmts₁ q

Tactic:
cases q <;> simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝¹ : Primcodable α
inst✝ : Inhabited α
p : Set α
⊢ ManyOneEquiv (toNat p) p

Tactic:
simp [ManyOneEquiv]

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : Set α
q : Set β
⊢ ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q

Tactic:
simp [ManyOneEquiv]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

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

Tactic:
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 mpr.cons.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t' : List α
U : List (List α)
helem : ∀ t ∈ t' :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = (t' :: U).flatten
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Tactic:
obtain - | ⟨b, t⟩ := t'
          · simp only [forall_eq_or_imp, List.mem_cons] at helem
            simp only [not_true, Ne, false_and] at helem
          simp only [List.flatten_cons, List.cons_append, List.cons_eq_cons] at hsum
          refine ⟨t, U.flatten, hsum.2, ?_, ?_⟩
          · specialize helem (b :: t) (by simp)
            rw [rmatch] at helem
            convert! helem.2
            exact hsum.1
          · grind

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

Goal state before:
pp: case prim.prec
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
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval ↑v = Part.some (pure (g v))
v : List.Vector ℕ (n + 1)
hf : cf.eval ↑v.tail = Part.some (pure (f v.tail))
⊢ (cf.prec cg).eval ↑(v.head ::ᵥ v.tail) =
    pure <$> (↑fun v ↦ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head) (v.head ::ᵥ v.tail)

Tactic:
replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail)

Goal state after:
case prim.prec
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 = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval ↑(a ::ᵥ b ::ᵥ v.tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval ↑(v.head ::ᵥ v.tail) =
    pure <$> (↑fun v ↦ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head) (v.head ::ᵥ v.tail)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
⊢ M q T.head = some (q', s) →
    Reaches₁ (TM1.step (tr M)) { l := some (Λ'.normal q), var := (), Tape := T }
      {
        l :=
          match
            match
              M q'
                (match s with
                  | TM0.Stmt.move d => Tape.move d T
                  | TM0.Stmt.write a => Tape.write a T).head with
            | some val => true
            | none => false with
          | true => some (Λ'.normal q')
          | false => none,
        var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
intro e

Goal state after:
case some
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
⊢ Reaches₁ (TM1.step (tr M)) { l := some (Λ'.normal q), var := (), Tape := T }
    {
      l :=
        match
          match
            M q'
              (match s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T).head with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg
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 : ℕ
h' : ¬k' = k
⊢ (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

Tactic:
· split_ifs <;> rw [Function.update_of_ne h', ← proj_map_nth, hL]
      rw [Function.update_of_ne h']

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

Goal state before:
pp: case pos.hn
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
i : ℕ
h : i = tl.length
⊢ (List.map some tl).length ≤ tl.length

Tactic:
List.length_map

Goal state after:
case pos.hn
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
i : ℕ
h : i = tl.length
⊢ tl.length ≤ tl.length