mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
h : ¬1 = 0
⊢ (s ∩ Function.support fun i ↦ 1).Infinite

Tactic:
simpa [Function.support_const h]

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case inl
α : Type u_1
s : Set α
hs : s.Infinite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

Tactic:
rw [hs.ncard]
    by_cases h : 1 = 0
    · simp [h]
    · exact finsum_mem_eq_zero_of_infinite (by simpa [Function.support_const h])

Goal state after:
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) - ↑(#K.verts) * ↑(#K.verts) +
    (↑(#K.verts) * (↑(#K.verts) - (↑t' - ↑t)) - ↑n * (↑(#K.verts) - (↑t' - ↑t)))

Tactic:
← add_sub_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) - ↑(#K.verts) * ↑(#K.verts) + ↑(#K.verts) * (↑(#K.verts) - (↑t' - ↑t)) -
    ↑n * (↑(#K.verts) - (↑t' - ↑t))
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) - ↑(#K.verts) * ↑(#K.verts) +
      (↑(#K.verts) * ↑(#K.verts) - ↑(#K.verts) * (↑t' - ↑t)) -
    ↑n * (↑(#K.verts) - (↑t' - ↑t))

Tactic:
← add_sub_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) - ↑(#K.verts) * ↑(#K.verts) + ↑(#K.verts) * ↑(#K.verts) -
      ↑(#K.verts) * (↑t' - ↑t) -
    ↑n * (↑(#K.verts) - (↑t' - ↑t))
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = w
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1

Tactic:
use v

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = w
⊢ (fun w_1 ↦ (G.subgraphOfAdj h).Adj v✝ w_1) v ∧ ∀ (y : V), (fun w_1 ↦ (G.subgraphOfAdj h).Adj v✝ w_1) y → y = v
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(G.degree a)

Tactic:
by
  rw [← sum_incMatrix_apply]
  simp only [mul_apply, incMatrix_apply', transpose_apply, mul_ite, mul_one, mul_zero]
  simp_all only [ite_true, sum_boole]

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

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ ↑(#{x | s(v, w) ∈ G.incidenceSet x}) = ↑2

Tactic:
← card_pair (G.ne_of_adj h)

Goal state after:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ ↑(#{x | s(v, w) ∈ G.incidenceSet x}) = ↑(#{(v, w).1, (v, w).2})
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
| ∑ i, ∑ j, if G.Adj j i then x i * x i - x i * x j else 0

Tactic:
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
| ∑ y, ∑ x_1, if G.Adj y x_1 then x x_1 * x x_1 - x x_1 * x y else 0
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), p.toSubgraph.Adj v w ↔ G.Adj v w

Tactic:
by
  refine fun w ↦ Subgraph.adj_iff_of_neighborSet_equiv (?_ : Nonempty _).some (Set.toFinite _)
  have := hp.ncard_neighborSet_toSubgraph_eq_two (by aesop)
  rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _),
    ← Set.cast_ncard (finite_neighborSet_toSubgraph p),
    hcyc
      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
        Set.nonempty_of_ncard_ne_zero <| by simp [this]),
    this]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert w₂ (insert x (t.erase b)))

Tactic:
exact hw.isNClique_snd_right.insert_insert_erase hbt hw.snd_notMem fun _ hz hZ ↦
               wa (h2t hz) (fun h ↦ haw <| (mem_insert.1 (h ▸ hz)).resolve_right hat) hZ

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

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) - (1 + 1) = n - (2 * k - μ) - 2

pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ w ∉ {v}

pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Tactic:
← Finset.compl_union

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - (1 + 1) = n - (2 * k - μ) - 2

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ w ∉ {v}

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset 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
hk : #(s ∩ t) = 0
⊢ X = univ

Tactic:
card_eq_zero

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
hk : s ∩ t = ∅
⊢ X = univ
Module: Mathlib.Combinatorics.Young.SemistandardTableau

Goal state before:
pp: μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
⊢ T i1 j ≤ T i2 j

Tactic:
by
  rcases eq_or_lt_of_le hi with h | h
  · rw [h]
  · exact le_of_lt (T.col_strict h cell)

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

Goal state before:
pp: m n : ℕ
⊢ m.psub' n = m.psub n

Tactic:
psub'

Goal state after:
m n : ℕ
⊢ (if n ≤ m then some (m - n) else none) = m.psub n
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 : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ ((f x).bind fun b ↦ some (g x b)) = Option.map (g x) (f x)

Tactic:
by cases f x <;> rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec fun a ↦ Vector.mOfFn fun i ↦ f i a

Tactic:
simp only [Vector.mOfFn, pure_eq_some, bind_eq_bind]

Goal state after:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec fun a ↦ (f 0 a).bind fun a_1 ↦ (Vector.mOfFn fun i ↦ f i.succ a).bind fun v ↦ Part.some (a_1 ::ᵥ v)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ ack m (n + 1) ≤ ack (m + 1) n

Tactic:
rcases n with - | n
  · simp
  · rw [ack_succ_succ]
    apply ack_mono_right m (le_trans _ <| add_add_one_le_ack _ n)
    lia

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 : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2
i : α
h₁ : 0 ≤ b i
⊢ b i * ↑n - ↑(r i n) = ‖b i * ↑n‖ - ‖↑(r i n)‖

Tactic:
by
      simp only [norm_mul, RCLike.norm_natCast, Real.norm_of_nonneg h₁]

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 - 2) * 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
h₁ : -1 + (-↑k - 1) = -↑k - 2
h₂ : -(↑k + 1) - 1 = -↑k - 2
⊢ 2 ^ (-↑k - 2) * x₀ ≤ z

Tactic:
exact hz.1

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
⊢ 1 ∈ Set.range fun p ↦ ∑ i, a i * b i ^ p

Tactic:
by
  refine mem_range_of_exists_le_of_exists_ge R.continuous_sumCoeffsExp ?le_one ?ge_one
  case le_one =>
    exact R.tendsto_zero_sumCoeffsExp.eventually_le_const zero_lt_one |>.exists
  case ge_one =>
    exact R.tendsto_atTop_sumCoeffsExp.eventually_ge_atTop _ |>.exists

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

Goal state before:

Tactic:
(fun x => deriv (fun z => z ^ (p a b)) x * (1 + ε x))
            _ =O[atTop] fun x => x ^ ((p a b) - 1) * (1 + ε x) :=
              IsBigO.mul (isBigO_deriv_rpow_const_atTop (p a b)) (isBigO_refl _ _)
            _ =O[atTop] fun x => x ^ ((p a b) - 1) * 1 :=
              IsBigO.mul (isBigO_refl _ _) isEquivalent_one_add_smoothingFn_one.isBigO
            _ = fun x => x ^ ((p a b) - 1) := by ext; rw [mul_one]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h : x ∈ evaln (k + 1) zero n
⊢ n < k + 1

Tactic:
rw [evaln] at h

Goal state after:
case zero
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure 0)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h : x ∈ evaln (k + 1) succ n
⊢ n < k + 1

Tactic:
rw [evaln] at h

Goal state after:
case succ
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure n.succ)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case left
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h : x ∈ evaln (k + 1) left n
⊢ n < k + 1

Tactic:
rw [evaln] at h

Goal state after:
case left
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).1)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case right
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h : x ∈ evaln (k + 1) right n
⊢ n < k + 1

Tactic:
rw [evaln] at h

Goal state after:
case right
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).2)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case pair
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h : x ∈ evaln (k + 1) (a✝¹.pair a✝) n
⊢ n < k + 1

Tactic:
rw [evaln] at h

Goal state after:
case pair
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) a✝¹ n <*> evaln (k + 1) a✝ n)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case comp
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h : x ∈ evaln (k + 1) (a✝¹.comp a✝) n
⊢ n < k + 1

Tactic:
rw [evaln] at h

Goal state after:
case comp
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        let x ← evaln (k + 1) a✝ n
        evaln (k + 1) a✝¹ x)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case prec
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h : x ∈ evaln (k + 1) (a✝¹.prec a✝) n
⊢ n < k + 1

Tactic:
rw [evaln] at h

Goal state after:
case prec
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) a✝¹ a) fun y ↦ do
                let i ← evaln k (a✝¹.prec a✝) (Nat.pair a y)
                evaln (k + 1) a✝ (Nat.pair a (Nat.pair y i)))
            n)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝ : Code
h : x ∈ evaln (k + 1) a✝.rfind' n
⊢ n < k + 1

Tactic:
rw [evaln] at h

Goal state after:
case rfind'
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) a✝ (Nat.pair a m)
              if x = 0 then pure m else evaln k a✝.rfind' (Nat.pair a (m + 1)))
            n)
      n
⊢ n < k + 1
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case a
α : 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
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ u ≤ n

Tactic:
exact le_of_lt hu.2

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

Goal state before:

Tactic:
1
        _ ≤ 2 * (c₁⁻¹ * c₁) * (1 / 2) := by
          rw [inv_mul_cancel₀ (by positivity : c₁ ≠ 0)]; norm_num
        _ = (2 * c₁⁻¹) * c₁ * (1 / 2) := by ring
        _ ≤ C * c₁ * (1 - ε n) := by gcongr

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

Goal state before:

Tactic:
‖g x‖ ≤ 1 / 2 * ‖f x‖ := hfg' x hbx
           _ = 1 / 2 * (-f x) := by congr; exact norm_of_nonpos (hf₂ x hbx)
           _ = _ := by ring

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

Goal state before:
pp: case hdb
α : 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
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ ↑u ^ (p a b + 1) ≤ ↑(r i n) ^ (p a b + 1)

Tactic:
exact rpow_le_rpow_of_nonpos (by positivity)
            (by exact_mod_cast hu.1) (le_of_lt hp)

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
x : List α
n : ℕ
⊢ x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l

Tactic:
by
  induction n generalizing x with
  | zero => simp
  | succ n ihn =>
    simp only [pow_succ', mem_mul, ihn]
    constructor
    · rintro ⟨a, ha, b, ⟨S, rfl, rfl, hS⟩, rfl⟩
      exact ⟨a :: S, rfl, rfl, forall_mem_cons.2 ⟨ha, hS⟩⟩
    · rintro ⟨_ | ⟨a, S⟩, rfl, hn, hS⟩ <;> cases hn
      rw [forall_mem_cons] at hS
      exact ⟨a, hS.1, _, ⟨S, rfl, rfl, hS.2⟩, rfl⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k : ℕ
c : Code
n : ℕ
⊢ ((List.range k)[n]?.bind fun a ↦ evaln k c a) = evaln k c n

Tactic:
by
  by_cases kn : n < k
  · simp [List.getElem?_range kn]
  · rw [List.getElem?_eq_none]
    · cases e : evaln k c n
      · rfl
      exact kn.elim (evaln_bound e)
    simpa using kn

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.prec
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      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 (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Nat.rec
      (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' + 1) (encode (cf.prec cg)))))
        (k' + 1, cf) (unpair n).1)
      (fun n_1 n_ih ↦
        (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' + 1) (encode (cf.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun i ↦
          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' + 1) (encode (cf.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    Nat.rec (evaln (k' + 1) cf (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2

Tactic:
rw [hg (Nat.pair_lt_pair_right _ lf)]

Goal state after:
case succ.prec
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      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 (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Nat.rec (evaln k cf (unpair n).1)
      (fun n_1 n_ih ↦
        (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' + 1) (encode (cf.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun i ↦
          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' + 1) (encode (cf.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    Nat.rec (evaln (k' + 1) cf (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2