mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ #↑s = #(↑s ⊕ ↑s)

Tactic:
← add_def,

Goal state after:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ #↑s = #↑s + #↑s
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r✝ r : ℕ
h : Maximal (fun H ↦ H.CliqueFree (r + 1 + 1)) G
⊢ G.Colorable (r + 1) ↔ G.IsCompleteMultipartite

Tactic:
refine ⟨fun hc ↦ ?_, fun hc ↦ hc.colorable_of_cliqueFree h.1⟩
    contrapose hc
    obtain ⟨_, _, _, _, _, hw⟩ :=
      exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hc
    exact hw.not_colorable_succ

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
⊢ p.IsHamiltonianCycle ↔ p.IsCycle ∧ p.length = Fintype.card α

Tactic:
by
  refine ⟨fun h ↦ ⟨h.isCycle, h.length_eq⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
  refine isHamiltonian_iff_isPath_and_length_eq.mpr ⟨h₁.isPath_tail, ?_⟩
  grind [length_tail_add_one, IsCycle.not_nil]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : (v : V) → Fintype ↑(M.neighborSet v)
⊢ M.IsPerfectMatching ↔ ∀ (v : V), M.degree v = 1

Tactic:
by
  simp [degree_eq_one_iff_existsUnique_adj, isPerfectMatching_iff]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
⊢ Even (Fintype.card ↑c.supp)

Tactic:
let : DecidablePred fun x ↦ x ∈ (M.induce c.supp).verts := fun a ↦ G.instDecidableMemSupp c a

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this : DecidablePred fun x ↦ x ∈ (M.induce c.supp).verts := fun a ↦ G.instDecidableMemSupp c a
⊢ Even (Fintype.card ↑c.supp)
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
⊢ (fun i ↦ if G.connectedComponentMk i = c then 1 else 0) ∈ (toLin' (lapMatrix ℝ G)).ker

Tactic:
rw [LinearMap.mem_ker, toLin'_apply, lapMatrix_mulVec_eq_zero_iff_forall_reachable]
  grind [ConnectedComponent.eq]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
⊢ w₁ ∈ W

Tactic:
simp [W]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
⊢ w₂ ∈ W

Tactic:
simp [W]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum = 0 ↔ G = ⊥

Tactic:
refine ⟨fun h ↦ ?_, by simp_all⟩
  simpa [h] using vertexCoverNum_exists G

Goal state after:
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 ≤ ENat.card V - (1 + 1)

Tactic:
ht₁,

Goal state after:
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
⊢ ↑(n - 1) ≤ ENat.card V - (1 + 1)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
c : α → Prop
inst✝ : DecidablePred c
f g : α → σ
hc : PrimrecPred c
hf : Primrec f
hg : Primrec g
⊢ Primrec fun a ↦ if c a then f a else g a

Tactic:
by
  simpa [Bool.cond_decide] using cond hc.decide hf hg

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst✝ : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
⊢ Nat.rec 0 (fun n IH ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) (f x) = Nat.findGreatest (p x) (f x)

Tactic:
induction f x

Goal state after:
case zero
α : Type u_1
inst✝¹ : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst✝ : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
⊢ Nat.rec 0 (fun n IH ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) 0 = Nat.findGreatest (p x) 0

case succ
α : Type u_1
inst✝¹ : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst✝ : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
n✝ : ℕ
a✝ : Nat.rec 0 (fun n IH ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) n✝ = Nat.findGreatest (p x) n✝
⊢ Nat.rec 0 (fun n IH ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) (n✝ + 1) =
    Nat.findGreatest (p x) (n✝ + 1)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
l₁ l₂ : List α
⊢ List.foldr (fun b s ↦ ((l₁, l₂), b, s).2.1 :: ((l₁, l₂), b, s).2.2) (l₁, l₂).2 (l₁, l₂).1 = l₁ ++ l₂

Tactic:
induction l₁

Goal state after:
case nil
α : Type u_1
inst✝ : Primcodable α
l₂ : List α
⊢ List.foldr (fun b s ↦ (([], l₂), b, s).2.1 :: (([], l₂), b, s).2.2) ([], l₂).2 ([], l₂).1 = [] ++ l₂

case cons
α : Type u_1
inst✝ : Primcodable α
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ :
  List.foldr (fun b s ↦ ((tail✝, l₂), b, s).2.1 :: ((tail✝, l₂), b, s).2.2) (tail✝, l₂).2 (tail✝, l₂).1 = tail✝ ++ l₂
⊢ List.foldr (fun b s ↦ ((head✝ :: tail✝, l₂), b, s).2.1 :: ((head✝ :: tail✝, l₂), b, s).2.2) (head✝ :: tail✝, l₂).2
      (head✝ :: tail✝, l₂).1 =
    head✝ :: tail✝ ++ l₂
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
⊢ n ∈ rfind p

Tactic:
let ⟨m, hm⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨_, h₁, fun {m} mn => (h₂ mn).fst⟩

Goal state after:
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
⊢ n ∈ rfind p
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec fun a ↦ (f 0 a).bind fun a_1 ↦ (Vector.mOfFn fun i ↦ f i.succ a).bind fun v ↦ Part.some (a_1 ::ᵥ v)

Tactic:
exact
      (hf 0).bind
        (Partrec.bind ((vector_mOfFn fun i => hf i.succ).comp fst)
          (Primrec.vector_cons.to_comp.comp (snd.comp fst) snd))

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: v : List.Vector ℕ 0
⊢ 0 = encode v

Tactic:
v.eq_nil

Goal state after:
v : List.Vector ℕ 0
⊢ 0 = encode nil
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
⊢ Partrec f.fix

Tactic:
let F : α → ℕ →. σ ⊕ α := fun a n =>
    n.rec (some (Sum.inr a)) fun _ IH => IH.bind fun s => Sum.casesOn s (fun _ => Part.some s) f

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
⊢ Partrec f.fix
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
⊢ (fun x ↦ p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)) =ᶠ[atTop] fun x ↦
    p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / log x ^ 2

Tactic:
by
      filter_upwards [eventually_gt_atTop 0] with x hx
      simp [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]

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

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 0
⊢ GrowsPolynomially fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖

Tactic:
| inr hp =>

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

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

Tactic:
| inr hp =>

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

Goal state before:
pp: case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ GrowsPolynomially fun x ↦ |f x|

Tactic:
have hmain : -f =ᶠ[atTop] fun x => |f x| := by
      filter_upwards [hf'] with x hx
      simp only [Pi.neg_apply, abs_of_nonpos hx]

Goal state after:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun x ↦ |f x|
⊢ GrowsPolynomially fun x ↦ |f x|
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case inr
α : 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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g ↑n

Tactic:
| inr hp =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) cf (Nat.pair a m)
              if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x
h :
  x ∈
    unpaired
      (fun a m ↦ do
        let x ← evaln (k + 1) cf (Nat.pair a m)
        if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
      n
⊢ x ∈
    unpaired
      (fun a m ↦ do
        let x ← evaln (k₂ + 1) cf (Nat.pair a m)
        if x = 0 then pure m else evaln k₂ cf.rfind' (Nat.pair a (m + 1)))
      n

Tactic:
simp? [Bind.bind, Option.bind_eq_some_iff] at h ⊢ says
        simp only [unpaired, bind, pair_unpair, Option.pure_def, Option.mem_def,
          Option.bind_eq_some_iff] at h ⊢

Goal state after:
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) cf (Nat.pair a m)
              if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x
h :
  ∃ a,
    evaln (k + 1) cf n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    evaln (k₂ + 1) cf n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case inr
α : 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₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n ≤ sumTransform (p a b) g (r i n) n

Tactic:
| inr hp =>

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

Goal state before:
pp: 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
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (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)
⊢ c₂⁻¹ > 0

Tactic:
change 0 < c₂⁻¹

Goal state after:
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
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (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)
⊢ 0 < c₂⁻¹
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case pos
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

pp: case neg
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : ¬shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

Tactic:
case neg => rw [IH s0]

Goal state after:
case pos
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hrf
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
z : Primrec fun a ↦ (unpair a.1.1.2).1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x ↦ lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))

Tactic:
have m := Primrec.snd.comp (Primrec.unpair.comp n)

Goal state after:
case hrf
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
z : Primrec fun a ↦ (unpair a.1.1.2).1
m : Primrec fun a ↦ (unpair a.1.1.2).2
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x ↦ lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: n : ℕ
⊢ (2 ^ n).size = n + 1

Tactic:
simpa [shiftLeft_eq, Nat.add_comm] using size_shiftLeft (m := 1) (by decide) n

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

Goal state before:
pp: case inr
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
⊢ ∃ 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:
| inr hp =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y ↦ do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this✝ : Partrec₂ g
cg : Code
eg : cg.eval = fun n ↦ (↑(decode n)).bind fun a ↦ Part.map encode ((fun p ↦ g p.1 p.2) a)
eg' : ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)
F : ℕ → Code := fun x ↦ f (cg.curry x)
this : Computable F
cF : Code
eF : cF.eval = fun n ↦ (↑(decode n)).bind fun a ↦ Part.map encode (↑F a)
⊢ cF.eval (encode cF) = Part.some (encode (F (encode cF)))

Tactic:
simp [eF]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
by
  rw [← cast_to_nat, to_of_nat]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton.mp
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ (∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) → ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
intro ⟨t, ht, h⟩
      obtain ⟨x', _, _⟩ := ih.mp ht
      rw [mem_εClosure_iff_exists] at h
      simp_rw [mem_εClosure_iff_exists_path] at h
      obtain ⟨u, _, n, _⟩ := h
      use x' ++ some a :: List.replicate n none
      rw [List.reduceOption_append, List.reduceOption_cons_of_some,
        List.reduceOption_replicate_none, isPath_append]
      tauto

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
⊢ append l₁ (mk l₂) = mk (l₁ ++ l₂)

Tactic:
induction l₁

Goal state after:
case nil
Γ : Type u_1
inst✝ : Inhabited Γ
l₂ : List Γ
⊢ append [] (mk l₂) = mk ([] ++ l₂)

case cons
Γ : Type u_1
inst✝ : Inhabited Γ
l₂ : List Γ
head✝ : Γ
tail✝ : List Γ
tail_ih✝ : append tail✝ (mk l₂) = mk (tail✝ ++ l₂)
⊢ append (head✝ :: tail✝) (mk l₂) = mk (head✝ :: tail✝ ++ l₂)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case left
Γ : 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
⊢ default ∈ ↑(trStmts M S)

Tactic:
apply Finset.mem_product.2

Goal state after:
case left
Γ : 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
⊢ default.1 ∈ TM1.stmts M S ∧ default.2 ∈ Finset.univ
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case h.right.head
α : 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 u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ a :: t ≠ [] ∧ P.rmatch (a :: t) = true

Tactic:
simp only [ne_eq, not_false_iff, true_and, rmatch, reduceCtorEq]
            exact ht

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L (ListBlank.cons a R)) =
      stepAux (f (enc (ListBlank.cons a R).head)) v
        (trTape' enc0 (ListBlank.cons (ListBlank.cons a R).head L) (ListBlank.cons a R).tail)

Tactic:
simp only [ListBlank.head_cons, ListBlank.tail_cons, trTape', ListBlank.cons_flatMap]

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v
        (Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯)
          (ListBlank.append (enc a).toList (R.flatMap (fun x ↦ (enc x).toList) ⋯))) =
      stepAux (f (enc a)) v
        (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯))
          (R.flatMap (fun x ↦ (enc x).toList) ⋯))