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

Goal state before:
pp: case cons
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j u✝ v✝ w✝ : V
hA : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h' : x v✝ = x w✝
⊢ x u✝ = x w✝

Tactic:
| cons hA _ h' =>

Goal state after:
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:
by
  rw [LinearMap.mem_ker, toLin'_apply, lapMatrix_mulVec_eq_zero_iff_forall_reachable]
  grind [ConnectedComponent.eq]

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ G.Adj (p.getVert n) v
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
⊢ v ∈ c'.supp

Tactic:
← hc',

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
⊢ v ∈ p.toSubgraph.verts
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
⊢ G.minDegree * (#W + 2 * k) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w

Tactic:
mul_add,

Goal state after:
α : 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
⊢ G.minDegree * #W + G.minDegree * (2 * k) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ ↑n
h₂ : ↑n ≤ ENat.card V
s : Set V
hs₁ : s.encard = G.vertexCoverNum
hs₂ : G.IsVertexCover s
r : Set V
hr₁ : s ⊆ r
left✝ : r ⊆ Set.univ
hr₃ : r.encard = ↑n
⊢ ∃ s, s.encard = ↑n ∧ G.IsVertexCover s

Tactic:
exact ⟨r, hr₃, hs₂.subset hr₁⟩

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

Goal state before:
pp: case refine_2
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
⊢ False

Tactic:
have : 1 < (Set.univ \ t).encard := by
    refine ENat.add_one_le_iff (by simp) |>.mp ?_
    rw [Set.encard_sdiff (by simp) (Set.finite_of_encard_eq_coe ht₁), Set.encard_univ]
    refine ENat.le_sub_of_add_le_left (by simp [ht₁]) ?_
    refine add_le_of_le_tsub_right_of_le (Order.add_one_le_of_lt ENat.one_lt_card) ?_
    grw [ht₁, ENat.natCast_sub, hn]
    simp [add_assoc, one_add_one_eq_two, le_tsub_add]

Goal state after:
case refine_2
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
this : 1 < (Set.univ \ t).encard
⊢ False
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m : ℕ
⊢ ppred 0 = some m ↔ m.succ = 0

Tactic:
constructor <;> intro h <;> contradiction

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
l : List (List α)
⊢ List.foldr (fun b s ↦ (fun x1 x2 ↦ x1 ++ x2) (l, b, s).2.1 (l, b, s).2.2) [] (id l) = l.flatten

Tactic:
dsimp; induction l <;> simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
l : List α
⊢ List.foldr (fun b s ↦ (fun a b ↦ (a, b).2.2.succ) (l, b, s).1 (l, b, s).2) 0 (id l) = l.length

Tactic:
dsimp; induction l <;> simp [*]

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

Goal state before:
pp: case zero
β : 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 σ := ⋯
bindList : β → ℕ → List β := ⋯
graph : β → ℕ → List (β × σ) := ⋯
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 : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph : ∀ {bs bs' : List β}, bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph (graph b i) (l b')))) (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
hi : 0 ≤ m b + 1
⊢ List.map (fun x ↦ (x, f x)) (bindList b (m b + 1 - 0)) = graph b 0

Tactic:
simpa [graph] using bindList_eq_nil

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun L b ↦ ∀ a ∈ L, R a b

Tactic:
by
  classical
  have h (L) (b) : (List.filter (R · b) L).length = L.length ↔ ∀ a ∈ L, R a b := by simp
  apply PrimrecRel.of_eq ?_ h
  exact (Primrec.eq.comp (list_length.comp <| PrimrecRel.listFilter hf) (.comp list_length fst))

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

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then f v - (f v).sqrt * (f v).sqrt else (f v).sqrt) =
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt)
      else ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt)).1

Tactic:
split_ifs <;> rfl

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

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v).sqrt else f v - (f v).sqrt * (f v).sqrt - (f v).sqrt) =
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt)
      else ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt)).2

Tactic:
split_ifs <;> rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : 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
hF : Partrec₂ F
p : α → ℕ → Part Bool := fun a n ↦ Part.map (fun s ↦ Sum.casesOn s (fun x ↦ true) fun x ↦ false) (F a n)
hp : Partrec₂ p
a : α
b : σ
⊢ (b ∈
      (Nat.rfind (p a)).bind fun b ↦
        (F (a, b).1 (a, b).2).bind fun b_1 ↦
          Sum.casesOn ((a, b), b_1).2 (fun b_2 ↦ Part.some (((a, b), b_1), b_2).2) fun b ↦ Part.none) ↔
    b ∈ f.fix a

Tactic:
by simpa [p] using fix_aux f _ _

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

Goal state before:
pp: ⊢ (fun n ↦ ↑n / log ↑n ^ 2) = fun n ↦ ↑n * (log ↑n ^ 2)⁻¹

Tactic:
simp_rw [div_eq_mul_inv]

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ z ^ (p - 1) / log z ^ 2) =o[atTop] fun z ↦ z ^ (p - 1) / 1

Tactic:
simp_rw [div_eq_mul_inv]

Goal state after:
p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ z ^ (p - 1) * (log z ^ 2)⁻¹) =o[atTop] fun z ↦ z ^ (p - 1) * 1⁻¹
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
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
⊢ (fun n ↦ q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n ↦ deriv q ↑n * (↑(r i n) - b i * ↑n)

Tactic:
obtain ⟨c₁, _, c₂, _, hq_poly⟩ := hq_poly b' hb

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x ↦ ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x ↦ ‖deriv q x‖) x) (c₂ * (fun x ↦ ‖deriv q x‖) x)
⊢ (fun n ↦ q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n ↦ deriv q ↑n * (↑(r i n) - b i * ↑n)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: c : ℝ
hc : c < 1
⊢ Tendsto (fun x ↦ 1 - ε x) atTop (𝓝 1)

Tactic:
rw [← isEquivalent_const_iff_tendsto one_ne_zero]

Goal state after:
c : ℝ
hc : c < 1
⊢ (fun x ↦ 1 - ε x) ~[atTop] Function.const ℝ 1
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (fun z ↦ -deriv ε z) =o[atTop] fun x ↦ x⁻¹

Tactic:
isLittleO_neg_left

Goal state after:
⊢ deriv ε =o[atTop] fun x ↦ x⁻¹
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
by
  by_cases! h : ∃ᶠ x in atTop, f x = 0
  · exact Or.inl <| eventually_zero_of_frequently_zero hf h
  · cases eventually_atTop_nonneg_or_nonpos hf with
    | inl h' =>
      refine Or.inr (Or.inl ?_)
      simp only [lt_iff_le_and_ne]
      rw [eventually_and]
      exact ⟨h', by filter_upwards [h] with x hx; exact hx.symm⟩
    | inr h' =>
      refine Or.inr (Or.inr ?_)
      simp only [lt_iff_le_and_ne]
      rw [eventually_and]
      exact ⟨h', h⟩

Goal state after:
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 : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ 1 * x

Tactic:
gcongr; exact le_of_lt hb.2

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
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
⊢ ↑n ^ p a b * (↑n - ↑(r i n)) * (c₂ * g ↑n / ↑n ^ (p a b + 1)) ≤ ↑n ^ p a b * ↑n * (c₂ * g ↑n / ↑n ^ (p a b + 1))

Tactic:
by
        gcongr; simp only [tsub_le_iff_right, le_add_iff_nonneg_right, Nat.cast_nonneg]

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

Goal state before:

Tactic:
f x + g x ≥ f x - ‖g x‖ := by
                rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le (g x)
           _ ≥ f x - 1 / 2 * f x := by gcongr
           _ = 1 / 2 * f x := by ring

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 ⊢
      refine h.imp fun x => And.imp (hf _ _) ?_
      by_cases x0 : x = 0 <;> simp [x0]
      exact evaln_mono hl'

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

Goal state before:

Tactic:
T n
    _ = (∑ i, a i * T (r i n)) + g n := R.h_rec n (by grind)
    _ ≤ (∑ i, a i * (C * ((1 - ε (r i n)) * asympBound g a b (r i n)))) + g n := by
      -- Apply the induction hypothesis
      gcongr (∑ i, a i * ?_) + g n with i _
      · exact le_of_lt <| R.a_pos _
      · exact h_ind (r i n) (by grind)
    _ = (∑ i, a i * (C * ((1 - ε (r i n)) * ((r i n) ^ (p a b)
              * (1 + (∑ u ∈ range (r i n), g u / u ^ ((p a b) + 1))))))) + g n := by
      simp_rw [asympBound_def']
    _ = (∑ i, C * a i * ((r i n) ^ (p a b) * (1 - ε (r i n))
              * ((1 + (∑ u ∈ range (r i n), g u / u ^ ((p a b) + 1)))))) + g n := by
      congr; ext; ring
    _ ≤ (∑ i, C * a i * ((b i) ^ (p a b) * n ^ (p a b) * (1 - ε n)
              * ((1 + (∑ u ∈ range (r i n), g u / u ^ ((p a b) + 1)))))) + g n := by
      gcongr (∑ i, C * a i * (?_
          * ((1 + (∑ u ∈ range (r i n), g u / u ^ ((p a b) + 1)))))) + g n with i
      · positivity [R.a_pos i]
      · refine add_nonneg zero_le_one <| Finset.sum_nonneg fun j _ => ?_
        rw [div_nonneg_iff]
        exact Or.inl ⟨R.g_nonneg j (by positivity), by positivity⟩
      · grind
    _ = (∑ i, C * a i * ((b i) ^ (p a b) * n ^ (p a b) * (1 - ε n)
              * ((1 + ((∑ u ∈ range n, g u / u ^ ((p a b) + 1))
              - (∑ u ∈ Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1))))))) + g n := by
      congr; ext i; congr
      refine eq_sub_of_add_eq ?_
      rw [add_comm]
      exact add_eq_of_eq_sub <| Finset.sum_Ico_eq_sub _
        <| le_of_lt <| R.r_lt_n i n <| n₀_ge_Rn₀.trans hn
    _ = (∑ i, C * a i * ((b i) ^ (p a b) * (1 - ε n) * ((n ^ (p a b)
              * (1 + (∑ u ∈ range n, g u / u ^ ((p a b) + 1)))
              - n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1))))))
              + g n := by
      congr; ext; ring
    _ = (∑ i, C * a i * ((b i) ^ (p a b) * (1 - ε n)
              * ((asympBound g a b n - sumTransform (p a b) g (r i n) n)))) + g n := by
      simp_rw [asympBound_def', sumTransform_def]
    _ ≤ (∑ i, C * a i * ((b i) ^ (p a b) * (1 - ε n)
              * ((asympBound g a b n - c₁ * g n)))) + g n := by
      gcongr with i
      · positivity [R.a_pos i]
      · positivity [R.b_pos i]
      · exact h_sumTransform i
    _ = (∑ i, C * (1 - ε n) * ((asympBound g a b n - c₁ * g n))
              * (a i * (b i) ^ (p a b))) + g n := by
      congr; ext; ring
    _ = C * (1 - ε n) * (asympBound g a b n - c₁ * g n) + g n := by
      rw [← Finset.mul_sum, R.sumCoeffsExp_p_eq_one, mul_one]
    _ = C * (1 - ε n) * asympBound g a b n + (1 - C * c₁ * (1 - ε n)) * g n := by ring
    _ ≤ C * (1 - ε n) * asympBound g a b n + 0 := by
      gcongr
      refine mul_nonpos_of_nonpos_of_nonneg ?_ g_pos
      rw [sub_nonpos]
      calc 1
        _ ≤ 2 * (c₁⁻¹ * c₁) * (1 / 2) := by
          rw [inv_mul_cancel₀ (by positivity : c₁ ≠ 0)]; norm_num
        _ = (2 * c₁⁻¹) * c₁ * (1 / 2) := by ring
        _ ≤ C * c₁ * (1 - ε n) := by gcongr
    _ = C * ((1 - ε n) * asympBound g a b n) := by ring

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:
mul_add,

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₀
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) + C * g ↑n = ∑ i, a i * (C * T (r i n)) + C * g ↑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
⊢ T =O[atTop] fun n ↦ (1 - ε ↑n) * asympBound g a b n

Tactic:
exact R.T_isBigO_smoothingFn_mul_asympBound

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

Goal state before:
pp: f : Bool → Bool → Bool
⊢ 0 = if f true false = true then 0 else 0

Tactic:
split_ifs <;> rfl

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

Goal state before:
pp: case bit
b : Bool
m : ℕ
e : m = 0 → b = true
IH : ∀ {n : ℕ}, m < 2 ^ n → m.size ≤ n
n : ℕ
h : bit b m < 2 ^ n
⊢ (bit b m).size ≤ n

Tactic:
rw [← Nat.bit_ne_zero_iff] at e
      rw [size_bit e]
      cases n with
      | zero => exact (e (Nat.lt_one_iff.mp h)).elim
      | succ n => exact succ_le_succ (IH (bit_lt_two_pow_succ_iff.mp h))

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

Goal state before:
pp: b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
i : ℕ
⊢ n.testBit i = false

Tactic:
← h (i + 1),

Goal state after:
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
i : ℕ
⊢ n.testBit i = (bit b n).testBit (i + 1)
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 : ℝ
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
⊢ (∀ (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)

Tactic:
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.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : PosNum
⊢ ↑↑n = ↑n

Tactic:
← to_nat_to_int,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : PosNum
⊢ ↑↑↑n = ↑n