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

Goal state before:
pp: case h
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ G.dist u v = G.diam

Tactic:
rw [diam, dist, congrArg ENat.toNat huv]

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

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : u ∈ Set.univ
⊢ u ∈ G.center

Tactic:
rw [mem_center_iff, h u]

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : u ∈ Set.univ
⊢ e = G.radius
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr.e_a.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) = r.choose 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1)

Tactic:
rw [Nat.choose_two_right, Nat.div_mul_cancel rd, mul_add_one, add_mul, ← add_assoc,
        ← add_rotate, add_comm _ (_ * _)]

Goal state after:
case inr.inr.e_a.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' * (r - 1) + n' % r * (n' / r) * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r) + n' % r * (n' / r) * (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ 2 * r * ((n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r)) + 2 * r * (n % r).choose 2 ≤ (r - 1) * n ^ 2

Tactic:
Nat.mul_div_le

Goal state after:
n r : ℕ
⊢ (n ^ 2 - (n % r) ^ 2) * (r - 1) + 2 * r * (n % r).choose 2 ≤ (r - 1) * n ^ 2
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'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
⊢ #({v_1 ∈ K.parts.disjiUnion id ⋯ | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) < #K.verts - t' + t

Tactic:
rw [filter_disjiUnion, card_disjiUnion, sum_eq_sum_sdiff_singleton_add hp]

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
⊢ ∑ x ∈ K.parts \ {p}, #({v_1 ∈ id x | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) +
      #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) <
    #K.verts - t' + t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Fintype V
inst✝⁵ : Fintype W
inst✝⁴ : Fintype α
inst✝³ : Fintype β
R : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : R
h : 0 ≤ x
⊢ x < ↑(zarankiewicz m n s t) ↔
    ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < ↑(#G.edgeFinset)

Tactic:
by
  simp_rw [← Nat.floor_lt h]
  exact lt_zarankiewicz_iff hm hn hs ht ⌊x⌋₊

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
⊢ G.Reachable a b

Tactic:
obtain ⟨_, p, hp⟩ := hG Fintype.one_lt_card.ne'

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w✝ : α
p : G.Walk w✝ w✝
hp : p.IsHamiltonianCycle
⊢ G.Reachable a b
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: 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
⊢ incMatrix R G a e * incMatrix R G b e = 0

Tactic:
incMatrix_apply_mul_incMatrix_apply,

Goal state after:
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
⊢ (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e = 0
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ ∑ j, incMatrix R G a j * incMatrix R G b j = 1

Tactic:
incMatrix_apply_mul_incMatrix_apply,

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ ∑ x, (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 x = 1
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
⊢ incMatrix R G * (incMatrix R G)ᵀ = of fun a b ↦ if a = b then ↑(G.degree a) else if G.Adj a b then 1 else 0

Tactic:
ext a b
  dsimp
  split_ifs with h h'
  · subst b
    exact incMatrix_mul_transpose_diag (R := R) G
  · exact G.incMatrix_mul_transpose_apply_of_adj h'
  · simp only [Matrix.mul_apply, Matrix.transpose_apply,
      G.incMatrix_apply_mul_incMatrix_apply_of_not_adj h h', sum_const_zero]

Goal state after:
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 - 0) =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
sub_zero

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) =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
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) + Fintype.card ↑(G.commonNeighbors v w) =
    2 * k - Fintype.card ↑(G.commonNeighbors v w) + Fintype.card ↑(G.commonNeighbors v w)

Tactic:
rw [Nat.sub_add_cancel, ← Set.toFinset_card]

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) + #(G.commonNeighbors v w).toFinset = 2 * k

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 ℓ μ
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ 2 * k
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' : ℕ
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'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
p₁ p₂ : ↥K.parts
heq : y ↑p₁ ⋯ = y ↑p₂ ⋯
hy₁' : y ↑p₁ ⋯ ⊆ ↑p₁ ∧ #(y ↑p₁ ⋯) = t
hy₂' : y ↑p₁ ⋯ ⊆ ↑p₂ ∧ #(y ↑p₁ ⋯) = t
⊢ (y ↑p₁ ?m.1277).Nonempty

Tactic:
rw [← Finset.card_pos, hy₁'.right]

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' : ℕ
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'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
p₁ p₂ : ↥K.parts
heq : y ↑p₁ ⋯ = y ↑p₂ ⋯
hy₁' : y ↑p₁ ⋯ ⊆ ↑p₁ ∧ #(y ↑p₁ ⋯) = t
hy₂' : y ↑p₁ ⋯ ⊆ ↑p₂ ∧ #(y ↑p₁ ⋯) = t
⊢ 0 < t
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ j < μ.rowLen i

Tactic:
rw [rowLen, Nat.lt_find_iff]

Goal state after:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ m ≤ j, ¬(i, m) ∉ μ
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ m ≤ j, (i, m) ∈ μ

Tactic:
exact ⟨fun h _ hmj => μ.up_left_mem (by rfl) hmj h, fun h => h _ (by rfl)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a ↦ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ (F a).2 = List.recOn (f a) (g a) fun b l IH ↦ h a (b, l, IH)

Tactic:
by
    suffices F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)) by rw [this]
    dsimp [F]
    induction f a <;> simp [*]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
⊢ a ∈ rfindOpt f

Tactic:
obtain ⟨k, hk⟩ := rfindOpt_spec ⟨h', rfl⟩

Goal state after:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
⊢ a ∈ rfindOpt f
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: 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
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x✝ y : ↑K.supp
hxy : x✝ ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x✝ ↑y
p : K.toSimpleGraph.Walk x✝ y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x✝ y
x a b : ↥K
hnxb : x ≠ b
hxa : Gmax.Adj ↑↑x ↑↑a
hxb : Gmax.Adj ↑↑a ↑↑b
hnadjxb : ¬Gmax.Adj ↑↑x ↑↑b
⊢ ∃ c, ↑↑a ≠ c ∧ ¬Gmax.Adj (↑↑a) c

Tactic:
simpa [universalVerts, IsUniversal] using a.1.2.2

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ 1) =o[atTop] fun z ↦ log z ^ 2

Tactic:
isLittleO_const_left

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ 1) =o[atTop] fun x ↦ log x ^ 2

Tactic:
isLittleO_const_left

Goal state after:
p : ℝ
hp : p ≠ 0
⊢ 1 = 0 ∨ Tendsto (Norm.norm ∘ fun x ↦ log x ^ 2) atTop atTop
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
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x ↦ ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x ↦ ‖deriv q x‖) x) (c₂ * (fun x ↦ ‖deriv q x‖) x)
h_tendsto : Tendsto (fun x ↦ b' * x) atTop atTop
n : ℕ
hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
h_ge_n₀ : R.n₀ ≤ n
h_n_pos : 0 < n
h_bn : 1 < b' * ↑n
⊢ ‖q ↑(r i n) - q (b i * ↑n)‖ ≤ c₂ * ‖deriv q ↑n * (↑(r i n) - b i * ↑n)‖

Tactic:
rw [norm_mul, ← mul_assoc]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x ↦ ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x ↦ ‖deriv q x‖) x) (c₂ * (fun x ↦ ‖deriv q x‖) x)
h_tendsto : Tendsto (fun x ↦ b' * x) atTop atTop
n : ℕ
hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
h_ge_n₀ : R.n₀ ≤ n
h_n_pos : 0 < n
h_bn : 1 < b' * ↑n
⊢ ‖q ↑(r i n) - q (b i * ↑n)‖ ≤ c₂ * ‖deriv q ↑n‖ * ‖↑(r i n) - b i * ↑n‖
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:

Tactic:
1 = exp 0 := by simp
         _ < exp 1 := by simp
         _ ≤ x := hx

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

Goal state before:

Tactic:
_ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u + 1 / 2 * f u := by gcongr
           _ = 3 / 2 * f u := by ring
           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = 3 * c₂ * (1 / 2 * f x) := by ring
           _ ≤ 3 * c₂ * (f x + g x) := by gcongr

Goal state after:
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
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.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 z := Primrec.fst.comp (Primrec.unpair.comp n)

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
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
z : Primrec fun a ↦ (unpair a.1.1.2).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.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
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
⊢ (1 + ε ↑n) * asympBound g a b n + (C - c₁ * (1 + ε ↑n)) * g ↑n ≥ (1 + ε ↑n) * asympBound g a b n + 0

Tactic:
by
      gcongr
      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was:
      `exact mul_nonneg (by grind +splitIndPred) g_pos` -/
      have : 1 + ε ↑n < 2 := by grind
      exact mul_nonneg (by grw [sub_nonneg, this, mul_comm, hC]) g_pos

Goal state after:
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
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
z✝¹ : Primrec fun a ↦ (unpair a.1.1.2).1
L : Primrec fun a ↦ a.1.1.1.1
z✝ : Primrec fun a ↦ (unpair a.1.1.1.2).1
y : Primrec Prod.snd
h₁ :
  Primrec fun a ↦
    lup (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).1
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).2.1
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).2.2
z : Primrec fun a ↦ (unpair a.1.1.1.1.2).1
⊢ Primrec fun p ↦
    (fun p i ↦
        lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1)
          (Nat.pair (unpair p.1.1.1.2).1 (Nat.pair p.2 i)))
      p.1 p.2

Tactic:
have y := y.comp (Primrec.fst (β := ℕ))

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
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
z✝¹ : Primrec fun a ↦ (unpair a.1.1.2).1
L : Primrec fun a ↦ a.1.1.1.1
z✝ : Primrec fun a ↦ (unpair a.1.1.1.2).1
y✝ : Primrec Prod.snd
h₁ :
  Primrec fun a ↦
    lup (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).1
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).2.1
      (a.1.1.1.1, (a.1.1.2, (ofNat (ℕ × Code) a.1.1.1.1.length).2), Nat.pair (unpair a.1.1.1.2).1 a.2).2.2
z : Primrec fun a ↦ (unpair a.1.1.1.1.2).1
y : Primrec fun a ↦ a.1.2
⊢ Primrec fun p ↦
    (fun p i ↦
        lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1)
          (Nat.pair (unpair p.1.1.1.2).1 (Nat.pair p.2 i)))
      p.1 p.2
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ M.accepts
hlen : Fintype.card σ ≤ x.length
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Tactic:
obtain ⟨_, a, b, c, hx, hlen, hnil, rfl, hb, hc⟩ := M.evalFrom_split (s := M.start) hlen rfl
  use a, b, c, hx, hlen, hnil
  intro y hy
  rw [Language.mem_mul] at hy
  rcases hy with ⟨ab, hab, c', hc', rfl⟩
  rw [Language.mem_mul] at hab
  rcases hab with ⟨a', ha', b', hb', rfl⟩
  rw [Set.mem_singleton_iff] at ha' hc'
  subst ha' hc'
  have h := M.evalFrom_of_pow hb hb'
  rwa [mem_accepts, eval, evalFrom_of_append, evalFrom_of_append, h, hc]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hrf
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
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x ↦ lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))

Tactic:
have z := Primrec.fst.comp (Primrec.unpair.comp n)

Goal state after:
case hrf
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
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
z : Primrec fun a ↦ (unpair a.1.1.2).1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x ↦ lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))
Module: Mathlib.Data.Nat.Size

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

Tactic:
simp [shiftLeft', Nat.pow_zero]

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

Goal state before:
pp: case bit
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
m i : ℕ
hn : (bit b n).testBit i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j
⊢ bit b n < m

Tactic:
| bit b n hn' =>

Goal state after: