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

Tactic:
← mul_assoc,

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)
| ↑(#K.verts) * (1 - 1 / ↑r + ε) * ↑n - ↑n * (↑(#K.verts) - (↑t' - ↑t)) - ↑(#K.verts) * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: 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
aux : ∀ {N N' : G.Subgraph}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
⊢ ∃! w, (M ⊔ M').Adj v w

Tactic:
cases Set.mem_or_mem_of_mem_union hv with
  | inl hmM => exact aux hM hd hmM
  | inr hmM' =>
    rw [sup_comm]
    exact aux hM' (Disjoint.symm hd) hmM'

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
⊢ ∃ M, M.IsPerfectMatching

Tactic:
obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂
  use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂
  have : p₁ ∪ Set.range (fun v ↦ (b v).1) = Set.univ := by
    rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
    exact union_eq_univ_of_forall_ncard_le h₁ h₂
  refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
  simp only [dite_else_false]
  split
  · exact existsUnique_eq'
  · obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩
    exact ⟨x, by grind⟩

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
__IsCycle✝ : (Walk.map f (cons y p)).IsCycle := IsCycle.map (Bijective.injective hf) (isCycle hp)
⊢ List.count x p.support = 1

Tactic:
simpa using hp.isHamiltonian_tail x

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

Goal state before:
pp: V✝ V : Type u_1
r v w : V
hadj : v ≠ w ∧ (v = r ∨ w = r)
h : v = r
⊢ (starGraph r).IsBridge s(v, w)

Tactic:
· subst h
    apply not_reachable_of_neighborSet_right_eq_empty hadj.1
    ext x
    aesop

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

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

Tactic:
← mul_assoc,

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 * ∑ x ∈ W, 1 + G.minDegree * 2 * ∑ x ∈ s ∩ t, 1 ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.edgeSet = G.edgeSet

Tactic:
← h.isTrail.isEulerian_iff

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.IsEulerian
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)
⊢ (?m.355 + 2).succ * ((2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) * (3 * r + 4).succ) ≤
    (?m.355 + 2).succ * ((3 * r + 2) * ‖α‖)

Tactic:
← mul_assoc,

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.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i : ℕ
h : i < μ.rowLens.length
⊢ μ.rowLens[i] = μ.rowLen i

Tactic:
by simp only [rowLens, List.getElem_range, List.getElem_map]

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∉ (cycles.connectedComponentMk c).supp
⊢ ¬(cycles.connectedComponentMk c).toSimpleGraph.spanningCoe.Adj x b

Tactic:
ConnectedComponent.adj_spanningCoe_toSimpleGraph

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∉ (cycles.connectedComponentMk c).supp
⊢ ¬(x ∈ (cycles.connectedComponentMk c).supp ∧ cycles.Adj x b)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Primrec (Function.uncurry f) ↔ Primrec₂ f

Tactic:
by
  rw [show Function.uncurry f = fun p : α × β => f p.1 p.2 from funext fun ⟨a, b⟩ => rfl]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
o : Option α
⊢ (Option.casesOn (id o) [] fun b ↦ [id b]) = o.toList

Tactic:
rcases o

Goal state after:
case none
α : Type u_1
inst✝ : Primcodable α
⊢ (Option.casesOn (id none) [] fun b ↦ [id b]) = none.toList

case some
α : Type u_1
inst✝ : Primcodable α
val✝ : α
⊢ (Option.casesOn (id (some val✝)) [] fun b ↦ [id b]) = (some val✝).toList
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case right
f : ℕ → ℕ
⊢ Nat.Partrec ↑fun n ↦ (unpair n).2

Tactic:
| right =>

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

Goal state before:
pp: ⊢ Primrec' fun v ↦ v.head - v.tail.head

Tactic:
by
  have : @Primrec' 2 fun v ↦ (fun a b ↦ b - a) v.head v.tail.head := by
    refine (prec head (pred.comp₁ _ (tail head))).of_eq fun v => ?_
    simp; induction v.head <;> simp [*, Nat.sub_add_eq]
  simpa using comp₂ (fun a b => b - a) this (tail head) head

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Partrec₂ fun a m ↦ Part.map (fun x ↦ x + m) (Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> f (Nat.pair a (n + m)))

Tactic:
by
    refine
      Partrec.map
        ((@Partrec₂.unpaired' fun a b : ℕ =>
              Nat.rfind fun n => (fun m => m = 0) <$> f (Nat.pair a (n + b))).1
          ?_)
        (Primrec.nat_add.comp Primrec.snd <| Primrec.snd.comp Primrec.fst).to_comp.to₂
    have : Nat.Partrec (fun a => Nat.rfind (fun n => (fun m => decide (m = 0)) <$>
      Nat.unpaired (fun a b => f (Nat.pair (Nat.unpair a).1 (b + (Nat.unpair a).2)))
        (Nat.pair a n))) :=
      rfind
        (Partrec₂.unpaired'.2
          ((Partrec.nat_iff.2 hf).comp
              (Primrec₂.pair.comp (Primrec.fst.comp <| Primrec.unpair.comp Primrec.fst)
                  (Primrec.nat_add.comp Primrec.snd
                    (Primrec.snd.comp <| Primrec.unpair.comp Primrec.fst))).to_comp))
    simpa

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

Goal state before:
pp: case right
n : ℕ
f✝ : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v ↦ (fun n ↦ (unpair n).2) v.head

Tactic:
| right =>

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case right
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun n ↦ (unpair n).2) n < ack m n

Tactic:
| right =>

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_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : f (2 ^ (-↑k - 1) * x₀) = 0
z : ℝ
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
hx : z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) → f z = 0
⊢ 2 ^ (-1) * (2 ^ (-↑k - 1) * x₀) ≤ z

Tactic:
← mul_assoc,

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_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : f (2 ^ (-↑k - 1) * x₀) = 0
z : ℝ
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
hx : z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) → f z = 0
⊢ 2 ^ (-1) * 2 ^ (-↑k - 1) * x₀ ≤ z
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 : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
i : α
hn : ↑n / log ↑n ^ 2 ≤ (1 - b (max_bi b)) / 2 * ↑n
⊢ (b i + (1 - b (max_bi b)) / 2) * ↑n ≤ (b (max_bi b) + (1 - b (max_bi b)) / 2) * ↑n

Tactic:
gcongr; exact max_bi_le _

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)
h_main_norm : (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)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ b i * ↑n ≤ 1 * ↑n

Tactic:
have := R.b_lt_one i; gcongr

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
heq : c₁ = c₂
c : ℝ
hc✝ : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
x : ℝ
hc : f x = c
⊢ f x ≤ 0

Tactic:
exact le_of_lt <| by simpa only [hc]

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)
h_main_norm : (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)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ b i * ↑n ≤ 1 * ↑n

Tactic:
have := R.b_lt_one i; gcongr

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_1.right
f : ℕ →. ℕ
⊢ ∃ c, c.eval = ↑fun n ↦ (unpair n).2

Tactic:
| right =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_2.right
⊢ Nat.Partrec right.eval

Tactic:
| right =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
⊢ x ∈ c.eval n

Tactic:
induction c generalizing x n <;> simp [eval, evaln, Option.bind_eq_some_iff, Seq.seq] at h ⊢ <;>
      obtain ⟨_, h⟩ := h

Goal state after:
case zero
k n x : ℕ
left✝ : n ≤ k
h : 0 = x
⊢ x ∈ pure 0 n

case succ
k n x : ℕ
left✝ : n ≤ k
h : n + 1 = x
⊢ x = n + 1

case left
k n x : ℕ
left✝ : n ≤ k
h : (unpair n).1 = x
⊢ x = (unpair n).1

case right
k n x : ℕ
left✝ : n ≤ k
h : (unpair n).2 = x
⊢ x = (unpair n).2

case pair
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h : ∃ a, evaln (k + 1) a✝¹ n = some a ∧ ∃ a_1, evaln (k + 1) a✝ n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ a ∈ a✝¹.eval n, ∃ a_1 ∈ a✝.eval n, Nat.pair a a_1 = x

case comp
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h : ∃ a, evaln (k + 1) a✝ n = some a ∧ evaln (k + 1) a✝¹ a = some x
⊢ ∃ a ∈ a✝.eval n, x ∈ a✝¹.eval a

case prec
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  Nat.rec (evaln (k + 1) a✝¹ (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k (a✝¹.prec a✝) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k + 1) a✝ (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    some x
⊢ x ∈
    Nat.rec (a✝¹.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ a✝.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
      (unpair n).2

case rfind'
k : ℕ
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  ∃ a,
    evaln (k + 1) a✝ n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k a✝.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    (0 ∈ a✝.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ a✝.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m))
⊢ (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
    ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)

Tactic:
hy₂

Goal state after:
case rfind'
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
⊢ ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
⊢ m∗ * n = n + m * (m∗ * n)

Tactic:
← mul_assoc,

Goal state after:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
⊢ m∗ * n = n + m * m∗ * n
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
w : ContextFreeRule T g.NT
l : w ∈ g.rules
r : w.Rewrites u v
⊢ ∃ r ∈ g.rules, Symbol.nonterminal r.input ∈ u

Tactic:
exact ⟨w, l, r.nonterminal_input_mem⟩

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

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

Tactic:
simp only [shiftLeft', ne_eq] at h ⊢

Goal state after:
case succ
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
⊢ (bit b (shiftLeft' b m n)).size = m.size + (n + 1)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case bit.bit
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap f) m n = bitwise f n m
bn : Bool
n : ℕ
hn : n = 0 → bn = true
a✝ : bitwise (swap f) (bit bm m) n = bitwise f n (bit bm m)
⊢ bitwise (swap f) (bit bm m) (bit bn n) = bitwise f (bit bn n) (bit bm m)

Tactic:
rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]

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

Goal state before:
pp: case succ
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
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2)
      (match Fin.ofNat 4 n with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0)
      [n + 1] =
    match Fin.ofNat 4 n + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
List.foldl_cons,

Goal state after:
case succ
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
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2)
      ((match Fin.ofNat 4 n with
        | 0 => n
        | 1 => 1
        | 2 => n + 1
        | 3 => 0) ^^^
        n + 1)
      [] =
    match Fin.ofNat 4 n + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit0.cmp b.bit0) (↑a.bit0 < ↑b.bit0) (a.bit0 = b.bit0) (↑b.bit0 < ↑a.bit0)

Tactic:
dsimp [cmp]

Goal state after:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) (a.cmp b)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit0.cmp b.bit1) (↑a.bit0 < ↑b.bit1) (a.bit0 = b.bit1) (↑b.bit1 < ↑a.bit0)

Tactic:
dsimp [cmp]

Goal state after:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
    (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (a.cmp b))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit1.cmp b.bit0) (↑a.bit1 < ↑b.bit0) (a.bit1 = b.bit0) (↑b.bit0 < ↑a.bit1)

Tactic:
dsimp [cmp]

Goal state after:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
    (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (a.cmp b))
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))

Tactic:
by
  simp_rw [stepSet, mem_iUnion₂, exists_prop]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
⊢ List.foldl M.stepSet (List.foldl M.stepSet (M.εClosure S) x) [a] = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a

Tactic:
List.foldl_cons,

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
⊢ List.foldl M.stepSet (M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a) [] =
    M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit1.cmp b.bit1) (↑a.bit1 < ↑b.bit1) (a.bit1 = b.bit1) (↑b.bit1 < ↑a.bit1)

Tactic:
dsimp [cmp]

Goal state after:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) (a.cmp b)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
dsimp [cmp]

Goal state after:
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) (a.cmp b) → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) (a.cmp b)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a : Num
ha : 0 < a
b c : Num
⊢ b < c → b * a < c * a

Tactic:
by
    revert ha
    transfer_rw
    apply flip mul_lt_mul_of_pos_right

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start

Tactic:
suffices εNFA.stepSet (toεNFA M) = stepSet M by rw [this]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ M.toεNFA.stepSet = M.stepSet
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case inr.inr
Γ : Type ?u.5
inst✝ : Inhabited Γ
l✝ : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
h₂ : n < (l ++ List.replicate i default).length
⊢ default = (l ++ List.replicate i default)[n]

Tactic:
List.getElem_append_right h,

Goal state after:
case inr.inr
Γ : Type ?u.5
inst✝ : Inhabited Γ
l✝ : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
h₂ : n < (l ++ List.replicate i default).length
⊢ default = (List.replicate i default)[n - l.length]