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

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

pp: case h9
α : 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
⊢ #(insert x (s.erase a) ∩ insert x (t.erase b)) = k + 1

Tactic:
case h8 => 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:
case h9
α : 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
⊢ #(insert x (s.erase a) ∩ insert x (t.erase b)) = k + 1
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg.inr.inl
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
rw [G'.adj_congr_of_sym2 (by grind : s(v, w) = s(u, x))]
    simp only [hnadj, false_iff, not_not]
    rcases hr.1 with ⟨rfl, rfl⟩ | ⟨hrr1, hrr2⟩
    · exact (hx' _ hww'.symm h1.symm).symm
    · grind

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

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

Tactic:
rw [decode_ofEquiv]
      cases (@decode α _ n) <;>
        simp [encode_ofEquiv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a))) =
    some (List.casesOn (f a) (g a) fun b l ↦ h a (b, l))

Tactic:
rcases f a with - | ⟨b, l⟩ <;> simp [encodek]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : ℕ → ℕ →. α
h : Partrec (Nat.unpaired f)
⊢ Partrec₂ f

Tactic:
by simpa using! Partrec.comp (g := fun p : ℕ × ℕ => (p.1, p.2)) h Primrec₂.pair.to_comp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun L b ↦ ∀ a ∈ L, R a b

Tactic:
have h (L) (b) : (List.filter (R · b) L).length = L.length ↔ ∀ a ∈ L, R a b := by simp

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
h : ∀ (L : List α) (b : β), (filter (fun x ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
⊢ PrimrecRel fun L b ↦ ∀ a ∈ L, R a b
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:
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₂

Goal state after:
f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Nat.Partrec (unpaired fun a b ↦ Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> f (Nat.pair a (n + b)))
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 - ↑n / log ↑n ^ 2 ≤ ↑(r i n)

Tactic:
rw [sub_le_iff_le_add, add_comm, ← 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
n : ℕ
hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2
i : α
h₁ : 0 ≤ b i
⊢ b i * ↑n - ↑(r i n) ≤ ↑n / log ↑n ^ 2
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)
⊢ ∃ u, G.IsTutteViolator u

Tactic:
cases nonempty_fintype V
  -- It suffices to consider the edge-maximal case
  obtain ⟨Gmax, hSubgraph, hMatchingFree, hMaximal⟩ := exists_maximal_isMatchingFree h
  refine ⟨Gmax.universalVerts, .mono hSubgraph ?_⟩
  by_contra! hc
  simp only [IsTutteViolator, Set.ncard_eq_toFinset_card', Set.toFinset_card] at hc
  by_cases! h' : ∀ (K : ConnectedComponent Gmax.deleteUniversalVerts.coe),
      Gmax.deleteUniversalVerts.coe.IsClique K.supp
  · -- Deleting universal vertices splits the graph into cliques
    rw [Fintype.card_eq_nat_card] at hc
    simp_rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at hc
    push Not at hc
    obtain ⟨M, hM⟩ := Subgraph.IsPerfectMatching.exists_of_isClique_supp hvEven
      (by simpa [IsTutteViolator] using hc) h'
    exact hMatchingFree M hM
  · -- Deleting universal vertices does not result in only cliques
    obtain ⟨K, hK⟩ := h'
    obtain ⟨x, y, hxy⟩ := (not_isClique_iff _).mp hK
    obtain ⟨p, hp⟩ := Reachable.exists_path_of_dist (K.connected_toSimpleGraph x y)
    obtain ⟨x, a, b, hxa, hxb, hnadjxb, hnxb⟩ := Walk.exists_adj_adj_not_adj_ne hp.2
      (p.reachable.one_lt_dist_of_ne_of_not_adj hxy.1 hxy.2)
    simp only [ConnectedComponent.toSimpleGraph, deleteUniversalVerts, universalVerts,
      Subgraph.verts_top, comap_adj, Function.Embedding.coe_subtype,
      Subgraph.coe_adj, Subgraph.induce_adj, Subtype.coe_prop, Subgraph.top_adj, true_and]
      at hxa hxb hnadjxb
    obtain ⟨c, hc⟩ : ∃ (c : V), (a : V) ≠ c ∧ ¬ Gmax.Adj a c := by
      simpa [universalVerts, IsUniversal] using a.1.2.2
    have hbnec : b.val.val ≠ c := by rintro rfl; exact hc.2 hxb
    obtain ⟨_, hG1⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rw [edge_le_iff (v := x.1.1) (w := b.1.1)]
      simp [hnadjxb, Subtype.val_injective.ne <| Subtype.val_injective.ne hnxb])
    obtain ⟨_, hG2⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rwa [edge_le_iff (v := a.1.1) (w := c), not_or])
    have hcnex : x.val.val ≠ c := by rintro rfl; exact hc.2 hxa.symm
    obtain ⟨Mcon, hMcon⟩ := tutte_exists_isPerfectMatching_of_near_matchings hxa
      hxb hnadjxb (fun hadj ↦ hc.2 hadj) (by lia) hcnex hc.1 hbnec hG1 hG2
    exact hMatchingFree Mcon hMcon

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 : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ logb 2 (x / x₀) ≤ 0

Tactic:
refine logb_nonpos (by norm_num) (by positivity) ?_

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 : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ x / x₀ ≤ 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_1.rfind
f f✝ : ℕ →. ℕ
pf : Nat.Partrec f✝
hf : ∃ c, c.eval = f✝
⊢ ∃ c, c.eval = fun a ↦ Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> f✝ (Nat.pair a n)

Tactic:
rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']

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

Goal state before:
pp: case hbc
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
hbx : b * x ≤ x
fx_nonneg : 0 ≤ f x
gx_nonneg : 0 ≤ g x
⊢ c₂ ≤ max c₂ c₄

Tactic:
exact le_max_left _ _

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

Goal state before:
pp: case hbc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ c₂ ≤ max c₂ (c₂ / c₁ ^ (p a b + 1))

Tactic:
exact le_max_left _ _

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.refine_1
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    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)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
⊢ 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)))
      m =
    some y

Tactic:
have := evaln_mono k.le_succ h₁
          simp [evaln, Option.bind_eq_some_iff] at this
          exact this.2

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
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
⊢ ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)) ≥
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / (c₁ * ↑n) ^ (p a b + 1))

Tactic:
gcongr n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / ?_)
          exact rpow_le_rpow_of_nonpos (by positivity) (hn₁ i) (le_of_lt hp)

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case mpr
α : Type u_1
l : Language α
x : List α
⊢ (∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []) → x ∈ l∗

Tactic:
rintro ⟨S, hx, h⟩
    exact ⟨S, hx, fun y hy ↦ (h y hy).1⟩

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:
induction n generalizing x with

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
⊢ l∗ * m ≤ m

Tactic:
rw [kstar_eq_iSup_pow, iSup_mul]
    refine iSup_le fun n ↦ ?_
    induction n with
    | zero => simp
    | succ n ih => grw [pow_succ, mul_assoc, h, ih]

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case cons
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
p' q' : List (Symbol T N)
hrs✝ : r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q')
⊢ ∃ p q,
    x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = p ++ [Symbol.nonterminal r.input] ++ q ∧
      x :: (p' ++ r.output ++ q') = p ++ r.output ++ q

Tactic:
use x :: p', q'

Goal state after:
case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
p' q' : List (Symbol T N)
hrs✝ : r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q')
⊢ x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = x :: p' ++ [Symbol.nonterminal r.input] ++ q' ∧
    x :: (p' ++ r.output ++ q') = x :: p' ++ r.output ++ q'
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ g.Derives u.reverse v.reverse ↔ g.reverse.Derives u v

Tactic:
← derives_reverse,

Goal state after:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ g.reverse.Derives u.reverse.reverse v.reverse.reverse ↔ g.reverse.Derives u v
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
| x ∈ List.map f ⁻¹' M.accepts

Tactic:
rw [Set.mem_preimage, mem_accepts]

Goal state after:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
| M.eval (List.map f x) ∈ M.accept
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
⊢ 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 n := n.comp (Primrec.fst (β := Code × Option ℕ))

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
⊢ 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 n : ℕ
h : m < 2 ^ n
⊢ m.size ≤ n

Tactic:
induction m using binaryRec' generalizing n with

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

Goal state before:
pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ (bit b✝ n✝).bits.length = (bit b✝ n✝).size

Tactic:
rw [size_bit, bits_append_bit _ _ h]
    · simp [ih]
    · simpa [bit_eq_zero_iff]

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

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun x ↦ f x ^ p) x) (c₂ * (fun x ↦ f x ^ p) x)

Tactic:
refine ⟨1, by norm_num, 1, by norm_num, ?_⟩

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (1 * (fun x ↦ f x ^ p) x) (1 * (fun x ↦ f x ^ p) x)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i ≠ true ∧ b.testBit i ≠ true ∧ c.testBit i ≠ true
⊢ v.testBit i ≠ true

Tactic:
simp_rw [Bool.eq_false_eq_not_eq_true] at hi ⊢

Goal state after:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i = false ∧ b.testBit i = false ∧ c.testBit i = false
⊢ v.testBit i = false
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ Countable { f // Partrec f }

Tactic:
apply Function.Surjective.countable (f := fun c => ⟨eval c, eval_part.comp (.const c) .id⟩)

Goal state after:
⊢ Function.Surjective fun c ↦ ⟨c.eval, ⋯⟩
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ pos p.succ = (pos p).succ

Tactic:
succ,

Goal state after:
p : PosNum
⊢ pos p.succ = pos (pos p).succ'
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range L.leftQuotient).Finite

Tactic:
rw [← hM, leftQuotient_accepts]

Goal state after:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range (M.acceptsFrom ∘ M.eval)).Finite
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
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ c₂ * (c₄ * ‖g x‖) = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖

Tactic:
simp [c₁_cancel]

Goal state after:
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
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ c₂ * (c₄ * |g x|) = c₂ * c₄ * |g x|
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially (g + (f - g))

Tactic:
exact add_isLittleO hg hf

Goal state after:
Module: Mathlib.Computability.TuringMachine.Tape

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

Tactic:
List.getI_eq_default _ h₂

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