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) * 1 - ↑(#K.verts) * (1 / ↑r) + ↑(#K.verts) * ε - (↑(#K.verts) - (↑t' - ↑t))) -
    ↑(#K.verts) * (↑t' - ↑t)

Tactic:
mul_one,

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) * (1 / ↑r) + ↑(#K.verts) * ε - (↑(#K.verts) - (↑t' - ↑t))) - ↑(#K.verts) * (↑t' - ↑t)
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
⊢ ∃ h, Bijective h ∧ ∀ (a : ↑p₁), G.Adj ↑a ↑(h a)

Tactic:
by
  classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : V) (h : x ∈ p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ h <| Set.mem_toFinset.mp <| hf₂ x
  have (x : V) (h : x ∈ p₂) : f x ∉ p₂ := h₁.disjoint |>.notMem_of_mem_left <|
    isBipartiteWith_neighborSet_subset h₁.symm h <| Set.mem_toFinset.mp <| hf₂ x
  have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]
  let f' (x : p₁) : p₂ := ⟨f x, by grind⟩
  let g' (x : p₂) : p₁ := ⟨f x, by grind⟩
  refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u : Set V
hc : G.IsClique u
hu : u.Finite
h : Even u.ncard
⊢ ∃ M, M.verts = u ∧ M.IsMatching

Tactic:
obtain ⟨t, u, rfl, hd, hcard⟩ := Set.exists_union_disjoint_ncard_eq_of_even h

Goal state after:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ ∃ M, M.verts = t ∪ u ∧ M.IsMatching
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ ↑(G.neighborSet v).ncard = Cardinal.mk ↑(p.toSubgraph.neighborSet v)

Tactic:
← Set.cast_ncard (finite_neighborSet_toSubgraph p),

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ ↑(G.neighborSet v).ncard = ↑(p.toSubgraph.neighborSet v).ncard
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.toSubgraph.Adj v w'

Tactic:
Walk.mem_support_iff_exists_getVert

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : ∃ n, p.getVert n = w' ∧ n ≤ p.length
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.toSubgraph.Adj v w'
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: case h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
j : V
⊢ ↑(∑ i, Quot.lift ↑x ⋯ i • G.lapMatrix_ker_basis_aux i) j = ↑x j

Tactic:
simp only [lapMatrix_ker_basis_aux]

Goal state after:
case h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
j : V
⊢ ↑(∑ x_1, Quot.lift ↑x ⋯ x_1 • ⟨fun i ↦ if G.connectedComponentMk i = x_1 then 1 else 0, ⋯⟩) j = ↑x j
Module: Mathlib.Combinatorics.SimpleGraph.LineGraph

Goal state before:
pp: V : Type u_1
⊢ ⊥.lineGraph = ⊥

Tactic:
aesop (add simp lineGraph)

Goal state after:
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_ne_1 : r ≠ 1
⊢ (1 - 1 / (↑r - 1) + 1 / (↑r - 1) * 1 * (1 / ↑r) + ε) * ↑n = (1 - 1 / ↑(r - 1) + ε') * ↑n

Tactic:
mul_one,

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_ne_1 : r ≠ 1
⊢ (1 - 1 / (↑r - 1) + 1 / (↑r - 1) * (1 / ↑r) + ε) * ↑n = (1 - 1 / ↑(r - 1) + ε') * ↑n
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
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card ↑(G.commonNeighbors v w)

Tactic:
apply Nat.add_right_cancel (m := Fintype.card (G.commonNeighbors v w))

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) + Fintype.card ↑(G.commonNeighbors v w) =
    2 * k - Fintype.card ↑(G.commonNeighbors v w) + Fintype.card ↑(G.commonNeighbors v w)
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
⊢ ∑ i ∈ W, G.minDegree * 1 + ∑ i ∈ s ∩ t, G.minDegree * 2 * 1 ≤ ∑ w ∈ W, G.degree w + ∑ i ∈ s ∩ t, 2 * G.degree i

Tactic:
mul_one,

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
⊢ ∑ x ∈ W, G.minDegree + ∑ x ∈ s ∩ t, G.minDegree * 2 ≤ ∑ w ∈ W, G.degree w + ∑ i ∈ s ∩ t, 2 * G.degree i
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 • 1 v w + ℓ • if G.Adj v w then 1 else 0) + μ • if v ≠ w ∧ ¬G.Adj v w then 1 else 0

Tactic:
simp only [Matrix.one_apply_ne' hn.symm, ne_eq, hn]
    by_cases ha : G.Adj v w <;>
      simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one,
        not_true_eq_false, not_false_eq_true, and_false, and_self]
    · rw [h.of_adj v w ha]
    · rw [h.of_not_adj hn ha]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
⊢ ∃ M, M.IsPerfectMatching

Tactic:
cases nonempty_fintype V
  obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
  obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card)
  refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
  · simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]
  · rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
    exact M.verts.union_compl_self

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

Goal state before:
pp: a b : ℕ × ℕ
a✝ : b ≤ a
h : a ∈ ↑∅
⊢ False

Tactic:
simp only [Finset.coe_empty, Set.mem_empty_iff_false] at h

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

Goal state before:
pp: α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode (decode n) = encode (decode n)

Tactic:
decode_ofEquiv

Goal state after:
α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode (decode n) = encode (Option.map (⇑e.symm) (decode n))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH : ∀ (l : List β) (x : σ), (G a)^[n] (x, l) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take n l), List.drop n l)
l : List β
x : σ
⊢ (G a)^[n] (G a (x, l)) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)

Tactic:
rcases l with - | ⟨b, l⟩ <;> simp [G, IH]

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

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i ↦ v.get i.succ) = f v.tail

Tactic:
← ofFn_get v.tail

Goal state after:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i ↦ v.get i.succ) = f (ofFn v.tail.get)
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
⊢ (match n.bodd, n.div2.bodd with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind').encodeCode =
    bit n.bodd (bit n.div2.bodd n.div2.div2) + 4

Tactic:
cases n.bodd

Goal state after:
case false
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
⊢ (match false, n.div2.bodd with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind').encodeCode =
    bit false (bit n.div2.bodd n.div2.div2) + 4

case true
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
⊢ (match true, n.div2.bodd with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind').encodeCode =
    bit true (bit n.div2.bodd n.div2.div2) + 4
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: ⊢ Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t

Tactic:
apply_rules [Primrec.nat_rec₁, primrec_pappAck_step.comp, Primrec.snd]

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

Goal state before:
pp: 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)

Tactic:
simp [hderiv, Real.deriv_rpow_const, neg_div, sub_eq_add_neg]

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
⊢ (∀ (i : α), r i n < n) → 0 < n → ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g ↑n

Tactic:
hr_lt_n

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
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
⊢ 0 < n → ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g ↑n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inl.inl
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
hmain : (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ |f x| * |g x|
⊢ GrowsPolynomially fun x ↦ f x * g x

Tactic:
iff_eventuallyEq hmain

Goal state after:
case inl.inl
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
hmain : (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ |f x| * |g x|
⊢ GrowsPolynomially fun x ↦ |f x| * |g x|
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_1.prec
f f✝ g✝ : ℕ →. ℕ
pf : Nat.Partrec f✝
pg : Nat.Partrec g✝
hf : ∃ c, c.eval = f✝
hg : ∃ c, c.eval = g✝
⊢ ∃ c,
    c.eval =
      unpaired fun a n ↦
        Nat.rec (f✝ a)
          (fun y IH ↦ do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

Tactic:
rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩

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, 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
⊢ (∀ (i : α), r i n < n) →
    0 < n → ∀ (i : α), min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n ≤ sumTransform (p a b) g (r i n) n

Tactic:
hr_lt_n

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, 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
⊢ 0 < n → ∀ (i : α), min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n ≤ sumTransform (p a b) g (r i n) n
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ ∀ (a : ContextFreeRule T g.reverse.NT),
    a ∈ g.reverse.rules ∧ a.Rewrites u.reverse v.reverse ↔
      (Equiv.ofBijective ContextFreeRule.reverse ⋯) a ∈ g.rules ∧
        ((Equiv.ofBijective ContextFreeRule.reverse ⋯) a).Rewrites u v

Tactic:
simp [ContextFreeRule.reverse_involutive.eq_iff]

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ ∀ (a : ContextFreeRule T g.reverse.NT),
    a ∈ g.reverse.rules ∧ a.Rewrites u v ↔
      (Equiv.ofBijective ContextFreeRule.reverse ⋯) a ∈ g.rules ∧
        ((Equiv.ofBijective ContextFreeRule.reverse ⋯) a).Rewrites u.reverse v.reverse

Tactic:
simp [ContextFreeRule.reverse_involutive.eq_iff]

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

Goal state before:
pp: case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hmain : (fun x ↦ (f x)⁻¹) =ᶠ[atTop] fun x ↦ |(f x)⁻¹|
⊢ GrowsPolynomially fun x ↦ (f x)⁻¹

Tactic:
iff_eventuallyEq hmain

Goal state after:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hmain : (fun x ↦ (f x)⁻¹) =ᶠ[atTop] fun x ↦ |(f x)⁻¹|
⊢ GrowsPolynomially fun x ↦ |(f x)⁻¹|
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
hmain : (fun x ↦ (f x)⁻¹) =ᶠ[atTop] fun x ↦ -|(f x)⁻¹|
⊢ GrowsPolynomially fun x ↦ (f x)⁻¹

Tactic:
iff_eventuallyEq hmain

Goal state after:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
hmain : (fun x ↦ (f x)⁻¹) =ᶠ[atTop] fun x ↦ -|(f x)⁻¹|
⊢ GrowsPolynomially fun x ↦ -|(f 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
⊢ T =O[atTop] asympBound g a b

Tactic:
by
  calc T
    _ =O[atTop] (fun n => (1 - ε n) * asympBound g a b n) := by
      exact R.T_isBigO_smoothingFn_mul_asympBound
    _ =O[atTop] (fun n => 1 * asympBound g a b n) := by
      refine IsBigO.mul (isBigO_const_of_tendsto (y := 1) ?_ one_ne_zero) (isBigO_refl _ _)
      rw [← Function.comp_def (fun n => 1 - ε n) Nat.cast]
      exact Tendsto.comp isEquivalent_one_sub_smoothingFn_one.tendsto_const
        tendsto_natCast_atTop_atTop
    _ = asympBound g a b := by simp

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
k₁ : ℕ
c₁ : Code
n₁ : ℕ
⊢ Nat.pair k₁ (encode c₁) < Nat.pair k (encode c) →
    lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair k (encode c))))
        (k₁, c₁) n₁ =
      evaln k₁ c₁ n₁

Tactic:
hl

Goal state after:
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
k₁ : ℕ
c₁ : Code
n₁ : ℕ
hl : Nat.pair k₁ (encode c₁) < Nat.pair k (encode c)
⊢ lup
      (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
        (List.range (Nat.pair k (encode c))))
      (k₁, c₁) n₁ =
    evaln k₁ c₁ n₁
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
hf_pos₂ : ∀ (y : ℝ), b * id x ≤ y → 0 < f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₂ ^ p * f x ^ p = (c₂ * f x) ^ p

Tactic:
mul_rpow (le_of_lt hc₂_mem) (le_of_lt 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 : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₂ ^ p * f x ^ p = c₂ ^ p * f x ^ p
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c : Code
n✝ x a m n : ℕ
⊢ m ≤ n → a ∈ evaln m c n✝ → a ∈ evaln n c n✝

Tactic:
hl

Goal state after:
c : Code
n✝ x a m n : ℕ
hl : m ≤ n
⊢ a ∈ evaln m c n✝ → a ∈ evaln n c n✝