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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑n * (↑(#K.verts) - ↑(#K.verts) * (1 / ↑r) + ↑(#K.verts) * ε - (↑(#K.verts) - (↑t' - ↑t))) - ↑(#K.verts) * (↑t' - ↑t)

Tactic:
sub_add_eq_add_sub,

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑n * (↑(#K.verts) + ↑(#K.verts) * ε - ↑(#K.verts) * (1 / ↑r) - (↑(#K.verts) - (↑t' - ↑t))) - ↑(#K.verts) * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inl
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hcx : C x = C v
y : α
hy : y ∈ insert w₂ ↑t
hcy : C y = C v
hx : x = w₁
⊢ False

Tactic:
cases hy with

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w ↦ N.Adj v w) w ∧ ∀ (y : V), (fun w ↦ N.Adj v w) y → y = w
y : V
hy : (N ⊔ N').Adj v y
⊢ y = w

Tactic:
cases hy with

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
b : ↑p₁ → ↑p₂
hb₁ : Bijective b
hb₂ : ∀ (a : ↑p₁), G.Adj ↑a ↑(b a)
⊢ p₁ ∪ Subtype.val '' Set.univ = Set.univ

Tactic:
Subtype.coe_image_univ

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
b : ↑p₁ → ↑p₂
hb₁ : Bijective b
hb₂ : ∀ (a : ↑p₁), G.Adj ↑a ↑(b a)
⊢ p₁ ∪ p₂ = Set.univ
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
⊢ Finite α

Tactic:
by
  have := hp.fintype; infer_instance

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

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = v
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1

Tactic:
use w; aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsPerfectMatching
c : G.ConnectedComponent
⊢ (M.induce c.supp).IsMatching

Tactic:
by
  simpa [h.2.verts_eq_univ] using h.1.induce_connectedComponent c

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

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : a = b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = ↑(G.degree a)

Tactic:
subst b
    exact incMatrix_mul_transpose_diag (R := R) G

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
⊢ A.IsHermitian

Tactic:
ext i j

Goal state after:
α : Type u_1
V : Type u_2
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
i j : V
⊢ Aᴴ i j = A i j
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun w ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun w ↦ M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Tactic:
right
    use w, w'
    aesop

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

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ↑(∑ c, ⟨g c • fun i ↦ if G.connectedComponentMk i = c then 1 else 0, ⋯⟩) = fun i ↦ g (G.connectedComponentMk i)

Tactic:
repeat rw [AddSubmonoid.coe_finsetSum]

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ∑ i, ↑⟨g i • fun i_1 ↦ if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩ = fun i ↦ g (G.connectedComponentMk i)
Module: Mathlib.Combinatorics.SimpleGraph.Partition

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → G.Partitionable n

Tactic:
rintro ⟨C⟩

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
⊢ G.Partitionable n
Module: Mathlib.Combinatorics.SimpleGraph.Partition

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype ↑C.colorClasses
⊢ h.toFinset.card ≤ Fintype.card (Fin n)

Tactic:
rw [h.card_toFinset]

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype ↑C.colorClasses
⊢ Fintype.card ↑C.colorClasses ≤ Fintype.card (Fin n)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w✝⁴ w✝³ w✝² : α
w✝¹ w✝ : Finset α
hw : H.IsFiveWheelLike (r + 1) k w✝⁴ w✝³ w✝² w✝¹ w✝
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5)

Tactic:
apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _

Goal state after:
α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w✝⁴ w✝³ w✝² : α
w✝¹ w✝ : Finset α
hw : H.IsFiveWheelLike (r + 1) k w✝⁴ w✝³ w✝² w✝¹ w✝
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (?m.355 + 2).succ * ((2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) * (3 * r + 4).succ) ≤
    (?m.355 + 2).succ * ((3 * r + 2) * ‖α‖)
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c d : Set V
hcd : c ⊆ d
hc : G.IsVertexCover c
⊢ G.IsVertexCover d

Tactic:
grind [IsVertexCover]

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

Goal state before:
pp: case refine_3
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ ¬(p.toSubgraph.spanningCoe ⊔ edge x a).Adj x b

pp: case refine_4
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
v w : V
hvw : (edge x a).Adj v w
⊢ (G ⊔ edge a c).Adj v w

Tactic:
· simp +contextual [hnpxb, edge_adj, hnab.symm]

Goal state after:
case refine_4
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
v w : V
hvw : (edge x a).Adj v w
⊢ (G ⊔ edge a c).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ ∃ G', G'.IsAlternating M.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
by
  refine ⟨p.toSubgraph.spanningCoe ⊔ edge x a, (hcalt.spanningCoe p.toSubgraph).sup_edge (by simpa)
    (fun u' hu'x hadj ↦ ?_) aux, ?_, ?_, by aesop, sup_le_iff.mpr ⟨hle, fun v w hvw ↦ ?_⟩⟩
  · simpa [← hp.snd_of_toSubgraph_adj hadj, hp.snd_of_toSubgraph_adj hpac]
  · refine hp.isCycles_spanningCoe_toSubgraph_sup_edge hgadj.ne.symm fun hadj ↦ ?_
    rw [← Walk.mem_edges_toSubgraph, Subgraph.mem_edgeSet] at hadj
    simp [← hp.snd_of_toSubgraph_adj hadj.symm, hp.snd_of_toSubgraph_adj hpac] at hnxc
  · simp +contextual [hnpxb, edge_adj, hnab.symm]
  · simpa [edge_adj, adj_congr_of_sym2 _ ((adj_edge _ _).mp hvw).1.symm] using .inl hgadj

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: w : List ℕ
hw : w.SortedGE
hpos : ∀ x ∈ w, 0 < x
⊢ (ofRowLens w hw).rowLens.length = w.length

Tactic:
by
  simp only [length_rowLens, colLen, Nat.find_eq_iff, mem_cells, mem_ofRowLens,
    lt_self_iff_false, IsEmpty.exists_iff, Classical.not_not]
  exact ⟨not_false, fun n hn => ⟨hn, hpos _ (List.getElem_mem hn)⟩⟩

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

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

Tactic:
rw [v.eq_nil]; rfl

Goal state after:
Module: Mathlib.Computability.Ackermann

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

Tactic:
simpa using one_lt_ack_succ_right m 0

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ 1 = 0 ∨ Tendsto (Norm.norm ∘ fun z ↦ log z ^ 2) atTop atTop

Tactic:
refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_

Goal state after:
p : ℝ
hp : p ≠ 0
⊢ Tendsto (fun z ↦ log z ^ 2) atTop atTop
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ 1 = 0 ∨ Tendsto (Norm.norm ∘ fun x ↦ log x ^ 2) atTop atTop

Tactic:
refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_

Goal state after:
p : ℝ
hp : p ≠ 0
⊢ Tendsto (fun x ↦ log x ^ 2) atTop atTop
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 c : ℝ
hc_mem : c ∈ Set.Ioo 0 1
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)
n : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * ↑n ≤ ↑(r i n)
i : α
h₁ : 0 < c
⊢ C = c * (C / c)

Tactic:
by
      rw [← mul_div_assoc]
      exact (mul_div_cancel_left₀ _ (by positivity)).symm

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
⊢ 0 ≤ -logb 2 (x / x₀)

Tactic:
neg_nonneg

Goal state after:
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₀) ≤ 0
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)
⊢ (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)‖

Tactic:
refine IsLittleO.eventuallyLE ?_

Goal state after:
α : 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)
⊢ (fun x ↦ q ↑(r i x) - q (b i * ↑x)) =o[atTop] fun x ↦ b i ^ p a b * ↑x ^ p a b * (ε (b i * ↑x) - ε ↑x)
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)
⊢ (fun n ↦ ↑n ^ p a b * (1 / log ↑n ^ 2)) =Θ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (1 / log ↑n ^ 2)

Tactic:
refine IsTheta.symm ?_

Goal state after:
α : 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)
⊢ (fun n ↦ b i ^ p a b * ↑n ^ p a b * (1 / log ↑n ^ 2)) =Θ[atTop] fun n ↦ ↑n ^ p a b * (1 / log ↑n ^ 2)
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)
⊢ (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)‖

Tactic:
refine IsLittleO.eventuallyLE ?_

Goal state after:
α : 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)
⊢ (fun x ↦ q ↑(r i x) - q (b i * ↑x)) =o[atTop] fun x ↦ b i ^ p a b * ↑x ^ p a b * (ε (b i * ↑x) - ε ↑x)
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)
⊢ (fun n ↦ ↑n ^ p a b * (1 / log ↑n ^ 2)) =Θ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (1 / log ↑n ^ 2)

Tactic:
refine IsTheta.symm ?_

Goal state after:
α : 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)
⊢ (fun n ↦ b i ^ p a b * ↑n ^ p a b * (1 / log ↑n ^ 2)) =Θ[atTop] fun n ↦ ↑n ^ p a b * (1 / log ↑n ^ 2)
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)
⊢ ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun x ↦ f x + g x) u ∈ Set.Icc (min c₁ c₃ * (fun x ↦ f x + g x) x) (c₂ * (fun x ↦ f x + g x) x)

Tactic:
refine ⟨max c₂ c₄, by change 0 < max c₂ c₄; positivity, ?_⟩

Goal state after:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg✝ : GrowsPolynomially g
hf' : 0 ≤ᶠ[atTop] f
hg' : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
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 : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun x ↦ f x + g x) u ∈ Set.Icc (min c₁ c₃ * (fun x ↦ f x + g x) x) (max c₂ c₄ * (fun x ↦ f x + g x) x)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_1.comp
f f✝ g✝ : ℕ →. ℕ
pf : Nat.Partrec f✝
pg : Nat.Partrec g✝
hf : ∃ c, c.eval = f✝
hg : ∃ c, c.eval = g✝
⊢ ∃ c, c.eval = fun n ↦ g✝ n >>= f✝

Tactic:
| comp pf pg hf hg =>

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

Goal state before:
pp: m k : ℕ
⊢ bit true (shiftLeft' true m k) + 1 = (m + 1) * 2 ^ (k + 1)

Tactic:
bit_val,

Goal state after:
m k : ℕ
⊢ 2 * shiftLeft' true m k + true.toNat + 1 = (m + 1) * 2 ^ (k + 1)
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ (bit b✝ n✝).bits.length = (bit b✝ n✝).size

Tactic:
size_bit,

Goal state after:
case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ (bit b✝ n✝).bits.length = n✝.size.succ

case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ bit b✝ n✝ ≠ 0
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
h : Even n
⊢ n ^^^ 1 = n + 1

Tactic:
by
  cases n with
  | zero => rfl
  | succ n =>
    simp +instances [HXor.hXor, instXorOp, xor, bitwise, even_iff.mp h, ← mul_two,
      div_two_mul_two_of_even h]

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

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ (n + 1 ^^^
      match 1 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) =
    match 1 + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
refine xor_one_of_even <| even_iff.mpr ?_

Goal state after:
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ (n + 1) % 2 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑↑p.bit0 = ↑p.bit0

Tactic:
by dsimp; rw [Nat.cast_add, p.cast_to_nat]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
⊢ M.toDFA.accepts = M.accepts

Tactic:
by
  ext x
  rw [mem_accepts, DFA.mem_accepts]
  constructor <;> · exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
m n : PosNum
⊢ ↑m = ↑n ↔ m = n

Tactic:
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
n : PosNum
⊢ 1 ≤ ↑n

Tactic:
rw [← cast_to_nat, ← Nat.cast_one, Nat.cast_le (α := α)]

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
n : PosNum
⊢ 1 ≤ ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: b : Bool
n : Num
⊢ ↑(bit b n) = Nat.bit b ↑n

Tactic:
cases b <;> cases n <;> simp [bit, two_mul] <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : Num
⊢ ↑m = ↑n ↔ m = n

Tactic:
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f a

Tactic:
refine ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_
    · refine PFun.mem_fix_iff.2 (Or.inl ?_)
      rw [h₂]
      apply Part.mem_some
    · refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH⟩)
      rw [h]
      apply Part.mem_some

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case single
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ b✝ : σ₁
ac : b✝ ∈ f₁ a₁
this :
  match f₁ a₁ with
  | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
  | none => f₂ a₂ = none
⊢ ∃ b₂, tr b✝ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
rwa [show f₁ a₁ = _ from ac] at this

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

Goal state before:
pp: case inr
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1) → l₁.length ≤ l₂.length → mk l₁ = mk l₂
h : ¬l₁.length ≤ l₂.length
⊢ mk l₁ = mk l₂

Tactic:
cases le_total l₁.length l₂.length <;> [skip; symm] <;> apply this <;> try assumption
    intro
    rw [H]

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b ↦ tr a = b
a₁ : σ₁
b₂ : σ₂
h✝ : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
h : tr b₁ ∈ eval f₂ (tr a₁)
⊢ b₂ ∈ eval f₂ (tr a₁)

Tactic:
rwa [bb] at h

Goal state after: