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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ᵥ* adjMatrix α G) v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
simp only [← dotProduct_adjMatrix, vecMul]
  refine congr rfl ?_; ext x
  rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : MulZeroOneClass α
d : V → α
⊢ diagonal d ⊙ adjMatrix α G = 0

Tactic:
by simp [diagonal_hadamard]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst✝ : DecidableEq α
i j : V
⊢ adjMatrix α h.toGraph i j = A i j

Tactic:
obtain h' | h' := h.zero_or_one i j <;> simp [h']

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : Even n
u v : Fin n
⊢ (cycleGraph n).Adj u v → decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)

Tactic:
hadj

Goal state after:
n : ℕ
h : Even n
u v : Fin n
hadj : (cycleGraph n).Adj u v
⊢ decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_2
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
hT' : T.IsTree
⊢ Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) T

Tactic:
rw [maximal_isAcyclic_iff_reachable_eq hT hT'.isAcyclic,
      T.preconnected_iff_reachable_eq_top.mp hT'.preconnected,
      G.preconnected_iff_reachable_eq_top.mp hG.preconnected]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : 2 ≤ n
u v : Fin n
⊢ (cycleGraph n).Adj u v → (if ↑u = n - 1 then 2 else ⟨↑u % 2, ⋯⟩) ≠ if ↑v = n - 1 then 2 else ⟨↑v % 2, ⋯⟩

Tactic:
hadj

Goal state after:
n : ℕ
h : 2 ≤ n
u v : Fin n
hadj : (cycleGraph n).Adj u v
⊢ (if ↑u = n - 1 then 2 else ⟨↑u % 2, ⋯⟩) ≠ if ↑v = n - 1 then 2 else ⟨↑v % 2, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
⊢ ¬G.IsCompleteMultipartite

Tactic:
by
  intro h
  have h0 : ¬ G.Adj (e 0) (e 1) := by simp [pathGraph_adj]
  have h1 : ¬ G.Adj (e 1) (e 2) := by simp [pathGraph_adj]
  have h2 : G.Adj (e 0) (e 2) := by simp [pathGraph_adj]
  exact h.trans _ _ _ h0 h1 h2

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
u v : V
⊢ G.Adj u v →
    (completeGraph (Fin 2)).Adj
      (let u_1 := verts (G.connectedComponentMk u);
      ⟨G.dist u_1 u % 2, ⋯⟩)
      (let u := verts (G.connectedComponentMk v);
      ⟨G.dist u v % 2, ⋯⟩)

Tactic:
hadj

Goal state after:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
u v : V
hadj : G.Adj u v
⊢ (completeGraph (Fin 2)).Adj
    (let u_1 := verts (G.connectedComponentMk u);
    ⟨G.dist u_1 u % 2, ⋯⟩)
    (let u := verts (G.connectedComponentMk v);
    ⟨G.dist u v % 2, ⋯⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ (turanGraph n (Fintype.card α - 1)).IsExtremal ⊤.Free

Tactic:
isExtremal_top_free_iff_isTuranMaximal

Goal state after:
n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ (turanGraph n (Fintype.card α - 1)).IsTuranMaximal (Fintype.card α - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hwc : w.IsCircuit
⊢ G.egirth ≤ ↑w.length

Tactic:
classical
  by_contra! hlg
  let w' : G.Walk a a := w.cycleBypass
  have hwc' : w'.IsCycle := hwc.isCycle_cycleBypass
  have hwlg' : w'.length < G.egirth := by
    grw [w.length_cycleBypass_le_length]
    exact hlg
  exact not_le_of_gt hwlg' (SimpleGraph.egirth_le_length hwc')

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

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hw : w.IsCycle
right✝ : G.egirth = ↑w.length
hG : G.IsAcyclic
⊢ False

Tactic:
exact hG _ hw

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

Goal state before:
pp: α : Type u_1
a b : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b s)
h3 : b ∉ s
ha : G.Adj a b
⊢ G.IsNClique (r + 1) (insert b (insert a s))

Tactic:
apply h1.insert (fun b hb ↦ ?_)

Goal state after:
α : Type u_1
a b✝ : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b✝ s)
h3 : b✝ ∉ s
ha : G.Adj a b✝
b : α
hb : b ∈ insert a s
⊢ G.Adj b✝ b
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'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ t'.choose t ^ r * t ≤ #(filter K t)

Tactic:
by
        refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt ht_lt_t')
        rw [← @Nat.cast_le ℝ, Nat.cast_mul _ (t' - t), Nat.cast_mul _ (t' - t),
          Nat.cast_sub ht_lt_t'.le]
        exact mul_le_card_filter_mul K hr_pos ht'_pos hδ (mod_cast hN)

Goal state after:
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
    | inl hy =>
    -- But this is a contradiction since `w₁` and `w₂` are adjacent.
      subst_vars; exact C.valid hw.isPathGraph3Compl.adj (hcy ▸ hcx)
    | inr hy =>
      apply (C.valid _ hcy.symm).elim
      exact hw.isNClique_right.1 (by simp) (by simp [hy]) fun h ↦ hw.notMem_right (h ▸ hy)

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support
v : V
hv : v ∈ (⨆ i, f i).verts
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun w ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun w ↦ (f i).Adj v w) y → y = w
y : V
hy : (⨆ i, f i).Adj v y
i' : ι
hi' : (f i').Adj v y
heq : i = i'
⊢ y = w

Tactic:
exact hw.2 y (heq.symm ▸ hi')

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

Goal state before:
pp: case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ e ∉ G.incidenceSet a ∩ G.incidenceSet b

Tactic:
rw [G.incidenceSet_inter_incidenceSet_of_not_adj h hab]

Goal state after:
case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ e ∉ ∅
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ ((∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
        ∑ i, ∑ j, if G.Adj j i then x i * x i - x i * x j else 0) /
      2 =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
conv_lhs => enter [1, 2]; rw [Finset.sum_comm]

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ ((∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
        ∑ y, ∑ x_1, if G.Adj y x_1 then x x_1 * x x_1 - x x_1 * x y else 0) /
      2 =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
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
h : Nonempty V
⊢ (lapMatrix ℝ G).det = 0

Tactic:
rw [← Matrix.exists_mulVec_eq_zero_iff]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : Nonempty V
⊢ ∃ v, v ≠ 0 ∧ lapMatrix ℝ G *ᵥ v = 0
Module: Mathlib.Combinatorics.SimpleGraph.Matching

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

Tactic:
hadj

Goal state after:
V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
⊢ p.toSubgraph.Adj 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)
x : α
hx : x ∈ Xᶜ
⊢ ∃ y ∈ s ∩ t, ¬G.Adj x y

Tactic:
contrapose! hx
      simpa [X] using hx

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

Goal state before:
pp: α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn n 1 fun n ↦ Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) = encode (decode n)

Tactic:
cases n with
      | zero => rfl
      | succ n =>
        rw [decode_option_succ]
        cases H : @decode α _ n <;> simp [H]

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

Goal state before:
pp: this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
⊢ ∀ (a : ℕ × ℕ) (b : ℕ),
    a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2 ↔ (fun x1 x2 ↦ x1 / x2) a.1 a.2 = b

Tactic:
rintro ⟨a, k⟩ q

Goal state after:
this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 ↦ x1 / x2) (a, k).1 (a, k).2 = q
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
⊢ Nat.Partrec ↑(unpaired fun z n ↦ Nat.rec (f✝ z) (fun y IH ↦ g✝ (Nat.pair z (Nat.pair y IH))) n)

Tactic:
refine (pf.prec pg).of_eq_tot fun n => ?_

Goal state after:
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
n : ℕ
⊢ unpaired (fun z n ↦ Nat.rec (f✝ z) (fun y IH ↦ g✝ (Nat.pair z (Nat.pair y IH))) n) n ∈
    unpaired
      (fun a n ↦
        Nat.rec (↑f✝ a)
          (fun y IH ↦ do
            let i ← IH
            ↑g✝ (Nat.pair a (Nat.pair y i)))
          n)
      n
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
i : ℕ
hi : i ≤ m b + 1
bindList_eq_nil : bindList b (m b + 1) = []
bs bs' : List β
has : bs' ⊆ bs
⊢ mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'

Tactic:
induction bs' with

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

Goal state before:
pp: H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (1 + 2)
⊢ ℕ

Tactic:
by
          have x := v.head; have y := v.tail.head
          exact if x.succ < y.succ * y.succ then y else y.succ

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

Goal state before:
pp: case inl
p : ℝ
hp : p = 0
⊢ GrowsPolynomially fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖

Tactic:
have h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 - ε z)) x‖)
        =ᶠ[atTop] fun z => z⁻¹ / (log z ^ 2) := by
      filter_upwards [eventually_deriv_one_sub_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos
      have : 0 ≤ x⁻¹ / (log x ^ 2) := by positivity
      simp only [hp, Real.rpow_zero, one_mul, hx, Real.norm_of_nonneg this]
    refine GrowsPolynomially.congr_of_eventuallyEq h₁ ?_
    refine GrowsPolynomially.div (GrowsPolynomially.inv growsPolynomially_id)
      (GrowsPolynomially.pow 2 growsPolynomially_log ?_)
    filter_upwards [eventually_ge_atTop 1] with _ hx using log_nonneg hx

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

Goal state before:
pp: p : ℝ
x✝ : p = 0 ∨ p ≠ 0
⊢ GrowsPolynomially fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖

Tactic:
cases eq_or_ne p 0 with

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

Goal state before:
pp: p : ℝ
x✝ : p = 0 ∨ p ≠ 0
⊢ GrowsPolynomially fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖

Tactic:
cases eq_or_ne p 0 with

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
⊢ Tendsto (fun p ↦ ∑ i, a i * b i ^ p) atBot atTop

Tactic:
by
  have h₁ : Tendsto (fun p : ℝ => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop :=
    Tendsto.const_mul_atTop (R.a_pos (max_bi b)) <| tendsto_rpow_atBot_of_base_lt_one _
      (by have := R.b_pos (max_bi b); linarith) (R.b_lt_one _)
  refine tendsto_atTop_mono (fun p => ?_) h₁
  refine Finset.single_le_sum (f := fun i => (a i : ℝ) * b i ^ p) (fun i _ => ?_) (mem_univ _)
  positivity [R.a_pos i, R.b_pos i]

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
n : ℕ
hn : 0 < n
⊢ ↑n ^ p a b * (1 + 0) ≤ asympBound g a b n

Tactic:
by
        simp only [asympBound_def']
        gcongr n ^ p a b * (1 + ?_)
        have := R.g_nonneg
        aesop (add safe Real.rpow_nonneg, safe div_nonneg, safe Finset.sum_nonneg)

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)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)
⊢ q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) ≤ q ↑(r i n)

Tactic:
sub_le_iff_le_add',

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)
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)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)
⊢ q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) + q ↑(r i n)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ 1 * x

Tactic:
by gcongr; exact le_of_lt hb.2

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hpr
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
⊢ Primrec fun a ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
    let y ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    some (Nat.pair x y)

Tactic:
have k := k.comp (Primrec.fst (β := Code × Code × Option ℕ × Option ℕ))

Goal state after:
case hpr
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
⊢ Primrec fun a ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
    let y ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    some (Nat.pair x y)
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
⊢ g.reverse.reverse = g

Tactic:
simp [reverse, Finset.map_map]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hco
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
⊢ Primrec fun a ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) x

Tactic:
have k := k.comp (Primrec.fst (β := Code × Code × Option ℕ × Option ℕ))

Goal state after:
case hco
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
⊢ Primrec fun a ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) x
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hpc
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    Nat.casesOn (unpair a.1.1.2).2 (lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) z) fun y ↦ do
      let i ← lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z y)
      lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) (Nat.pair z (Nat.pair y i))

Tactic:
have k := k.comp (Primrec.fst (β := Code × Code × Option ℕ × Option ℕ))

Goal state after:
case hpc
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    Nat.casesOn (unpair a.1.1.2).2 (lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) z) fun y ↦ do
      let i ← lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z y)
      lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) (Nat.pair z (Nat.pair y i))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ 1 * x

Tactic:
by gcongr; exact le_of_lt hb.2

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
⊢ M.acceptsFrom (S ∪ T) = M.acceptsFrom S + M.acceptsFrom T

Tactic:
by
  rw [Language.add_def]; ext x
  simp only [mem_acceptsFrom, evalFrom_union, mem_union]
  constructor
  · rintro ⟨s, hs, h | h⟩
    · left; tauto
    · right; tauto
  · rintro (⟨s, hs, h⟩ | ⟨s, hs, h⟩) <;> exists s <;> tauto

Goal state after: