mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ 2 ≤ G.ediam

Tactic:
by_contra

Goal state after:
case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
this : ¬2 ≤ G.ediam
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ t.encard ≠ ⊤

Tactic:
by simp [ht₁]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
K : G.deleteUniversalVerts.coe.ConnectedComponent
this : G.IsClique (Subtype.val '' K.supp \ M1.verts)
⊢ Even (Subtype.val '' K.supp \ M1.verts).ncard

Tactic:
hM1.1

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
K : G.deleteUniversalVerts.coe.ConnectedComponent
this : G.IsClique (Subtype.val '' K.supp \ M1.verts)
⊢ Even (Subtype.val '' K.supp \ (Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t)).ncard
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.liftOn' groupElts (fun g ↦ g • ↑(↑ps index)) ⋯).Nonempty ↔ (↑(↑ps index)).Nonempty

Tactic:
rw [← groupElts.out_eq', Quotient.liftOn'_mk'']

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.out groupElts • ↑(↑ps index)).Nonempty ↔ (↑(↑ps index)).Nonempty
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.liftOn' groupElts (fun g ↦ g • ↑(↑ps index)) ⋯).Finite ↔ (↑(↑ps index)).Finite

Tactic:
rw [← groupElts.out_eq', Quotient.liftOn'_mk'']

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.out groupElts • ↑(↑ps index)).Finite ↔ (↑(↑ps index)).Finite
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
i : ℕ
hi : i ≤ m b + 1
bindList_m_lt : ∀ (k : ℕ), ∀ b' ∈ bindList b k, m b' < m b + 1 - k
b' : β
ha' : b' ∈ bindList b (m b + 1)
⊢ False

Tactic:
by_contra

Goal state after:
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝¹ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this✝ : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
i : ℕ
hi : i ≤ m b + 1
bindList_m_lt : ∀ (k : ℕ), ∀ b' ∈ bindList b k, m b' < m b + 1 - k
b' : β
ha' : b' ∈ bindList b (m b + 1)
this : ¬False
⊢ False
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
⊢ (((↑(decode n)).bind fun a ↦ Part.map encode (↑f a)).bind fun n_1 ↦
      Nat.rec ((↑(decode n)).bind fun a ↦ Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode ((fun p ↦ h p.1 p.2) a))
        n_1) =
    (↑(decode n)).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (f a)) a)

Tactic:
rcases e : decode (α := α) n with - | a
    · simp
    · simp only [coe_some, PFun.coe_val, bind_some]
      induction f a <;> simp_all

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: c : Code
⊢ (pappAck.step c).eval 0 = c.eval 1

Tactic:
by
  simp [pappAck.step, Code.eval]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: c : Code
n : ℕ
⊢ (pappAck.step c).eval (n + 1) = ((pappAck.step c).eval n).bind c.eval

Tactic:
by
  simp [pappAck.step, Code.eval]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ (pappAck m).eval n = Part.some (ack m n)

Tactic:
by
  induction m, n using ack.induct with
    | case1 n => simp [Code.eval, pappAck]
    | case2 m hm => simp [pappAck, hm]
    | case3 m n hmn₁ hmn₂ => dsimp only [pappAck] at *; simp [hmn₁, hmn₂]

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ Tendsto (fun x ↦ log x ^ 2) atTop atTop

Tactic:
exact Tendsto.comp (g := fun z => z ^ 2)
              (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop

Goal state after:
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
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < asympBound g a b n

Tactic:
by
  filter_upwards [eventually_gt_atTop 0] with n hn using R.asympBound_pos n hn

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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
⊢ q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)

Tactic:
exact hn

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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)
⊢ q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)

Tactic:
exact hn

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : ℕ →. ℕ
⊢ Nat.Partrec f ↔ ∃ c, c.eval = f

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
  · rintro ⟨c, rfl⟩
    induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'

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 : α), 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
⊢ C * (∑ i, a i * T (r i n) + g ↑n) = ∑ i, a i * (C * T (r i n)) + C * g ↑n

Tactic:
rw [mul_add, mul_sum]; grind

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

Goal state before:
pp: case bit
b : Bool
n : ℕ
h : n = 0 → b = true
IH : n < 2 ^ n.size
⊢ bit b n < 2 ^ (bit b n).size

Tactic:
rw [← Nat.bit_ne_zero_iff] at h
    rwa [size_bit h, bit_lt_two_pow_succ_iff]

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

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

Tactic:
filter_upwards [eventually_gt_atTop 0, hfnew, hpos,
          (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hpos]
          with x _ hf₁ hf_pos hf_pos₂

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_pos : 0 < f x
hf_pos₂ : ∀ (y : ℝ), b * id x ≤ y → 0 < f y
⊢ ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (c₂ ^ p * f x ^ p) (c₁ ^ p * f x ^ p)
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
L : Language α
h : L.IsRegular
σ : Type
w✝ : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ M.toNFA.reverse.toDFA.accepts = L.reverse

Tactic:
by ext; simp [hM]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case step
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
n : ℕ
h✝ : M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ n, M.IsPath s₁ t✝ (List.replicate n none)

Tactic:
use n + 1

Goal state after:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
n : ℕ
h✝ : M.IsPath s₁ s✝ (List.replicate n none)
⊢ M.IsPath s₁ t✝ (List.replicate (n + 1) none)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝² x✝¹ x✝ : Num
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
simp_rw [← to_nat_inj, mul_to_nat, mul_assoc]

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

Goal state before:
pp: n : PosNum
⊢ ↑↑n = pos n

Tactic:
← of_to_nat n

Goal state after:
n : PosNum
⊢ ↑↑n = ↑↑n
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ M.toεNFA.evalFrom start = M.evalFrom start

Tactic:
by
  rw [evalFrom, εNFA.evalFrom, toεNFA_εClosure]
  suffices εNFA.stepSet (toεNFA M) = stepSet M by rw [this]
  ext S s
  simp only [stepSet, εNFA.stepSet, exists_prop, Set.mem_iUnion]
  apply exists_congr
  simp only [and_congr_right_iff]
  intro _ _
  rw [M.toεNFA_εClosure]
  rfl

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' fun v ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
g : ℕ → Part ℕ := fun n₁ ↦ (↑(decode n₁)).bind fun a ↦ Part.map encode (f a)
i : List.Vector ℕ n
⊢ g (encode i) = f i

Tactic:
dsimp only [g]

Goal state after:
this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' fun v ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
g : ℕ → Part ℕ := fun n₁ ↦ (↑(decode n₁)).bind fun a ↦ Part.map encode (f a)
i : List.Vector ℕ n
⊢ ((↑(decode (encode i))).bind fun a ↦ Part.map encode (f a)) = f i
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case nil.zero
Γ : Type ?u.5
inst✝ : Inhabited Γ
l : ListBlank Γ
⊢ BlankExtends [].tail ([] ++ List.replicate 0 default).tail

Tactic:
exact ⟨0, rfl⟩

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

Goal state before:
pp: case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = if 0 = n + 1 then f (L.nth 0) else L.nth 0

Tactic:
if_neg (Nat.succ_ne_zero _).symm

Goal state after:
case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = L.nth 0
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case pos.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
refine ⟨t, u, h.2, ?_, hQ⟩

Goal state after:
case pos.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ (P.deriv a).rmatch t = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
⊢ ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
rcases Finite.exists_equiv_fin Γ with ⟨n, ⟨e⟩⟩

Goal state after:
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
⊢ ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
refine ⟨t, u, h.2, ?_, hQ⟩

Goal state after:
case neg.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ (P.deriv a).rmatch t = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
l₁ l₂ : List Bool
e : (enc a).toList = l₁.reverseAux l₂
⊢ (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
induction l₁ generalizing l₂ with
  | nil => cases e; rfl
  | cons b l₁ IH =>
    simp only [List.length, iterate_succ_apply]
    convert! IH e
    simp only [ListBlank.tail_cons, ListBlank.append, Tape.move_left_mk', ListBlank.head_cons]

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ (addBottom L).head.1 = true

Tactic:
by
  rw [addBottom, ListBlank.head_cons]

Goal state after:
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
⊢ ListBlank.map (proj k') (ListBlank.modifyNth (fun a ↦ update a k (some (f v))) (S k).length L) =
    ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse

Tactic:
refine ListBlank.ext fun i ↦ ?_

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 : ℕ
⊢ (ListBlank.map (proj k') (ListBlank.modifyNth (fun a ↦ update a k (some (f v))) (S k).length L)).nth i =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i
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
⊢ ListBlank.map (proj k') (ListBlank.modifyNth (fun a ↦ update a k none) tl.length L) =
    ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse

Tactic:
refine ListBlank.ext fun i ↦ ?_

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 : ℕ
⊢ (ListBlank.map (proj k') (ListBlank.modifyNth (fun a ↦ update a k none) tl.length L)).nth i =
    (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
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
z : ↑Z.toTop
⊢ (ConcreteCategory.hom a) z = (ConcreteCategory.hom b) z

Tactic:
apply_fun (fun q ↦ q z) at hfst hsnd

Goal state after:
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 = (ConcreteCategory.hom b) z
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: ⊢ trNat 0 = []

Tactic:
rw [trNat, Nat.cast_zero]; rfl

Goal state after: