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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ ↑(t'.choose t) ^ r * ↑t + ↑r * ↑t' ≤ (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * ((↑t' - ↑t) / (↑r * ↑t' * ε - ↑t))

Tactic:
le_mul_iff_one_le_right (by positivity),

Goal state after:
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ 1 ≤ (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)
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)))
x✝ : α
hx : x✝ ∈ X
h : #({z ∈ W | ¬G.Adj x✝ z}) < 3
⊢ ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x✝ y

Tactic:
simpa [X] using hx

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)
x : α
hx : ∀ y ∈ s ∩ t, G.Adj x y
⊢ x ∉ Xᶜ

Tactic:
simpa [X] using hx

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

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2

Tactic:
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl,
    Set.toFinset_sdiff, Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
  simp_rw [compl_neighborFinset_sdiff_inter_eq]
  have hne : v ≠ w := ne_of_adj _ ha
  rw [compl_adj] at ha
  rw [card_sdiff_of_subset, ← insert_eq, card_insert_of_notMem, card_singleton,
    ← Finset.compl_union]
  · rw [card_compl, h.card_neighborFinset_union_of_not_adj hne ha.2, ← h.card]
  · simp only [hne.symm, not_false_iff, mem_singleton]
  · intro u
    simp only [mem_union, mem_compl, mem_neighborFinset, mem_inter, mem_singleton]
    rintro (rfl | rfl) <;> simpa [adj_comm] using ha.2

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

Goal state before:
pp: case convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #((G.neighborFinset w ∩ (G.neighborFinset v)ᶜ) \ {v}) = k - ℓ - 1

Tactic:
← sdiff_eq_inter_compl,

Goal state after:
case convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #((G.neighborFinset w \ G.neighborFinset v) \ {v}) = k - ℓ - 1
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case inr
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) =
    (k • 0 + ℓ • if G.Adj v w then 1 else 0) + μ • if ¬False ∧ ¬G.Adj v w then 1 else 0

Tactic:
by_cases ha : G.Adj v w

Goal state after:
case pos
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : G.Adj v w
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) =
    (k • 0 + ℓ • if G.Adj v w then 1 else 0) + μ • if ¬False ∧ ¬G.Adj v w then 1 else 0

case neg
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬G.Adj v w
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) =
    (k • 0 + ℓ • if G.Adj v w then 1 else 0) + μ • if ¬False ∧ ¬G.Adj v w then 1 else 0
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case nil
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens [] ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]

Tactic:
rw [YoungDiagram.cellsOfRowLens]

Goal state after:
case nil
c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens (head✝ :: tail✝) ↔ ∃ (h : c.1 < (head✝ :: tail✝).length), c.2 < (head✝ :: tail✝)[c.1]

Tactic:
rw [YoungDiagram.cellsOfRowLens]

Goal state after:
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : c.1 < (head✝ :: tail✝).length), c.2 < (head✝ :: tail✝)[c.1]
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ (Nat.casesOn (encode (o a)) (Option.some (f a)) fun n ↦ Option.map (g a) (decode n)) =
    Option.some (Option.casesOn (o a) (f a) (g a))

Tactic:
cases o a <;> simp [encodek]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
⊢ Nat.rec (Option.some [])
      (fun y IH ↦
        (a, y, IH).2.2.bind fun b ↦
          Option.map (fun b_1 ↦ (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2])
            (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2))
      a.2 =
    Option.some ((fun a n ↦ List.map (f a) (List.range n)) a.1 a.2)

Tactic:
by
      induction a.2 with
      | zero => rfl
      | succ n IH => simp [IH, H, List.range_succ]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ (ofNatCode (n + 4)).encodeCode = n + 4

Tactic:
conv_rhs => rw [← Nat.bit_bodd_div2 n, ← Nat.bit_bodd_div2 n.div2]

Goal state after:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ (ofNatCode (n + 4)).encodeCode = bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ ack 1 n = n + 2

Tactic:
induction n with
  | zero => simp
  | succ n IH => simp [IH]

Goal state after:
Module: Mathlib.Computability.Ackermann

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

Tactic:
by
    rw [ack_succ_zero]
    apply one_lt_ack_succ_left

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

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

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

Tactic:
· -- Deleting universal vertices splits the graph into cliques
    rw [Fintype.card_eq_nat_card] at hc
    simp_rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at hc
    push Not at hc
    obtain ⟨M, hM⟩ := Subgraph.IsPerfectMatching.exists_of_isClique_supp hvEven
      (by simpa [IsTutteViolator] using hc) h'
    exact hMatchingFree M hM

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

Goal state before:
pp: ⊢ ¬Primrec fun n ↦ ack n n

Tactic:
rw [Primrec.nat_iff]
  exact not_nat_primrec_ack_self

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

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

Tactic:
by
    filter_upwards [eventually_gt_atTop 1, eventually_deriv_one_sub_smoothingFn]
      with x hx hderiv
    rw [hderiv, Real.deriv_rpow_const]

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

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

Tactic:
filter_upwards [eventually_gt_atTop 1, eventually_deriv_one_add_smoothingFn]
        with x hx hderiv

Goal state after:
p x : ℝ
hx : 1 < x
hderiv : deriv (fun x ↦ 1 + ε x) x = -x⁻¹ / log x ^ 2
⊢ deriv (fun x ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x ↦ 1 + ε x) x =
    p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖) =Θ[atTop] fun z ↦ z ^ (p - 1)

Tactic:
by
  refine IsTheta.norm_left ?_
  calc (fun x => deriv (fun z => z ^ p * (1 + ε z)) x) =Θ[atTop] fun z => p * z ^ (p - 1) :=
      (isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn hp).isTheta
    _ =Θ[atTop] fun z => z ^ (p - 1) := IsTheta.const_mul_left hp <| isTheta_refl _ _

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
i : α
⊢ (fun n ↦ (log ↑n - log (b i) - log ↑n) / ((log (b i) + log ↑n) * log ↑n)) = fun n ↦
    -log (b i) / ((log (b i) + log ↑n) * log ↑n)

Tactic:
ext; congr; ring

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 > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g ↑n

Tactic:
obtain ⟨c₂, hc₂_mem, hc₂⟩ := R.g_grows_poly.eventually_atTop_le_nat hc₁_mem

Goal state after:
α : 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
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g ↑n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

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

Tactic:
· 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.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:
by
          refine IsTheta.symm ?_
          simp_rw [mul_assoc]
          refine IsTheta.const_mul_left ?_ (isTheta_refl _ _)
          have := R.b_pos i; positivity

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 * ∑ _u ∈ Ico (r i n) n, c₂ * g ↑n / ↑n ^ (p a b + 1) ≤
    ↑n ^ p a b * #(Ico (r i n) n) • (c₂ * g ↑n / ↑n ^ (p a b + 1))

Tactic:
by
        gcongr; exact Finset.sum_le_card_nsmul _ _ _ (fun x _ => by rfl)

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

Goal state before:
pp: case ha
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := ⋯
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) 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
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, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
i : α
a✝ : i ∈ univ
⊢ 0 ≤ 1 + ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1)

Tactic:
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⟩

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 cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        let x ← evaln (k + 1) cg n
        evaln (k + 1) cf x)
      n =
    some x
h :
  x ∈ do
    let x ← evaln (k + 1) cg n
    evaln (k + 1) cf x
⊢ x ∈ do
    let x ← evaln (k₂ + 1) cg n
    evaln (k₂ + 1) cf x

Tactic:
simp only [bind, 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 cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        let x ← evaln (k + 1) cg n
        evaln (k + 1) cf x)
      n =
    some x
h : ∃ a, evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
⊢ ∃ a, evaln (k₂ + 1) cg n = some a ∧ evaln (k₂ + 1) cf a = some x
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case ha
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := ⋯
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
i : α
a✝ : i ∈ univ
⊢ 0 ≤ 1 + ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1)

Tactic:
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⟩

Goal state after:
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 = n✝.size.succ

pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ bit b✝ n✝ ≠ 0

Tactic:
bits_append_bit _ _ h

Goal state after:
case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ (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.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
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ^ p ≤ c₂ ^ p * f x ^ p

Tactic:
calc
      (f u) ^ p ≤ (c₂ * f x) ^ p := by gcongr; exact (hf₁ u hu).2
        _ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]

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

Goal state before:
pp: a b : Num
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by simp only [← lt_to_nat, ← le_to_nat, lt_iff_le_not_ge]

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 → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)

Tactic:
suffices ∀ q, SupportsStmt S q → (∀ q' ∈ writes q, q' ∈ trSupp M S) →
        SupportsStmt (trSupp M S) (trNormal dec q) ∧
        ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q') by
      rcases Finset.mem_biUnion.1 h with ⟨l, hl, h⟩
      have :=
        this _ (ss.2 _ hl) fun q' hq ↦ Finset.mem_biUnion.2 ⟨_, hl, Finset.mem_insert_of_mem hq⟩
      rcases Finset.mem_insert.1 h with (rfl | h)
      exacts [this.1, this.2 _ h]

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
⊢ ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S q →
      (∀ q' ∈ writes q, q' ∈ trSupp M S) →
        SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑0 = ↑(pos one) >>> (n + 1)

Tactic:
rw [Nat.shiftRight_eq_div_pow]

Goal state after:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑0 = ↑(pos one) / 2 ^ (n + 1)
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P✝¹ : TopCat → Prop
α : Type w
inst✝³ : Finite α
X : α → CompHausLike P✝¹
inst✝² : HasExplicitFiniteCoproduct X
P✝ : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P✝
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
⊢ PreservesFiniteCoproducts (compHausLikeToTop P)

Tactic:
by
  refine ⟨fun n ↦ ⟨fun {F} ↦ ?_⟩⟩
  suffices PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P) from
    preservesColimit_of_iso_diagram _ Discrete.natIsoFunctor.symm
  exact preservesColimit_of_preserves_colimit_cocone (CompHausLike.finiteCoproduct.isColimit _)
    ((isColimitMapCoconeCofanMkEquiv _ _ _).2 (TopCat.sigmaCofanIsColimit _))

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

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

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

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

Goal state before:
pp: case fix
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal f (Cont.fix f k) v) k v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)

Tactic:
rw [cont_eval_fix IHf]

Goal state after: