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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ((f y).firstDart ⋯).toProd = (y, x)

Tactic:
rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ((cons ⋯ (f x)).firstDart ⋯).toProd = (y, x)

case contra
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
K : Finset V
left✝ : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
⊢ ∃ a ∈ K, ∃ b ∈ K, a ≠ b ∧ ¬G.Adj a b

Tactic:
by
    simpa only [isNClique_iff, IsClique, Set.Pairwise, mem_coe, ne_eq, and_true, not_forall,
      exists_prop, exists_and_right] using h K

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

Goal state before:
pp: n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (Even x ↔ Even y)

Tactic:
simp [Nat.even_iff]

Goal state after:
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (x % 2 = 0 ↔ y % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
x y : V
h : G.Adj x y
hbr : ¬G.IsBridge s(x, y)
⊢ (G.deleteEdges {s(x, y)}).edgeFinset.card < G.edgeFinset.card

Tactic:
exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]

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

Goal state before:
pp: n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (Even x ↔ Even y)

Tactic:
simp [Nat.even_iff]

Goal state after:
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (x % 2 = 0 ↔ y % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

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

Tactic:
intro u v hadj
    match n with
    | 0 => exact u.elim0
    | 1 => simp at h
    | n + 2 =>
      simp only [cycleGraph_adj] at hadj
      split_ifs with hu hv
      · simp [Fin.eq_mk_iff_val_eq.mpr hu, Fin.eq_mk_iff_val_eq.mpr hv] at hadj
      · refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val (?_))).symm
        exact v.val.mod_lt Nat.zero_lt_two
      · refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val ?_))
        exact u.val.mod_lt Nat.zero_lt_two
      · simp only [ne_eq, Fin.ext_iff]
        have hu' : u.val + (1 : Fin (n + 2)) < n + 2 := by fin_omega
        have hv' : v.val + (1 : Fin (n + 2)) < n + 2 := by fin_omega
        cases hadj with
        | inl huv | inr huv =>
          rw [← add_eq_of_eq_sub' huv.symm]
          simp only [Fin.val_add_eq_of_add_lt hv', Fin.val_add_eq_of_add_lt hu', Fin.val_one]
          rw [show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; lia,
            Nat.even_add]
          simp only [Nat.not_even_one, iff_false, not_iff_self, iff_not_self]
          exact id

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.IsTree
u : V
⊢ ∀ {v w : V}, G.Adj v w → ⟨G.dist u v % 2, ⋯⟩ ≠ ⟨G.dist u w % 2, ⋯⟩

Tactic:
grind [dist_eq_dist_add_one_of_adj]

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

Goal state before:
pp: case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ u ∈ ⊥.center

Tactic:
rw [mem_center_iff, eccent_bot, radius_bot]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v w u✝ v✝ w✝ : ↑Kᶜ
a : (induce Kᶜ G).Adj u✝ v✝
q : (induce Kᶜ G).Walk v✝ w✝
ih : q.IsPath → f ⋯ = f ⋯
⊢ (Walk.cons a q).IsPath → f ⋯ = f ⋯

Tactic:
rename_i u v w

Goal state after:
case cons
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v✝ w✝ u v w : ↑Kᶜ
a : (induce Kᶜ G).Adj u v
q : (induce Kᶜ G).Walk v w
ih : q.IsPath → f ⋯ = f ⋯
⊢ (Walk.cons a q).IsPath → f ⋯ = f ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

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

Tactic:
tsub_mul,

Goal state after:
n r : ℕ
⊢ n ^ 2 * (r - 1) - (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✝ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
hs' : s ∈ powersetCard t p
w : Fin n
hw : w ∈ s
⊢ ?m.317

Tactic:
rw [mem_powersetCard] at hs

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✝¹ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs✝ : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
hs : s ⊆ {v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v} ∧ #s = t
hs' : s ∈ powersetCard t p
w : Fin n
hw : w ∈ s
⊢ ?m.327 hs' w hw
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w ↦ N.Adj v w) w ∧ ∀ (y : V), (fun w ↦ N.Adj v w) y → y = w
⊢ ∀ (y : V), (fun w ↦ (N ⊔ N').Adj v w) y → y = w

Tactic:
intro y hy

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w ↦ N.Adj v w) w ∧ ∀ (y : V), (fun w ↦ N.Adj v w) y → y = w
y : V
hy : (N ⊔ N').Adj v y
⊢ y = w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
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), (fun w ↦ (⨆ i, f i).Adj v w) y → y = w

Tactic:
intro y hy

Goal state after:
case h
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
⊢ y = w
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
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ {x | True ∧ (x = a ∨ x = b)} = {a, b}

Tactic:
ext e

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e✝ : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
e : α
⊢ e ∈ {x | True ∧ (x = a ∨ x = b)} ↔ e ∈ {a, b}
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
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ ↑2 = ↑(p.toSubgraph.neighborSet v).ncard

Tactic:
hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)

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
this : (G.neighborSet v).Nonempty
⊢ ↑2 = ↑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
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2

Tactic:
card_sdiff_of_subset,

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)ᶜ) - #({w} ∪ {v}) = 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} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ ⋯.edgesFinset = G.edgeFinset

Tactic:
ext e

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
⊢ e ∈ ⋯.edgesFinset ↔ e ∈ G.edgeFinset
Module: Mathlib.Combinatorics.Young.SemistandardTableau

Goal state before:
pp: μ : YoungDiagram
i✝ j1✝ j2✝ : ℕ
hj : j1✝ < j2✝
hcell : (i✝, j2✝) ∈ μ
⊢ (if (i✝, j1✝) ∈ μ then i✝ else 0) ≤ if (i✝, j2✝) ∈ μ then i✝ else 0

Tactic:
by
    rw [if_pos hcell, if_pos (μ.up_left_mem (by rfl) (le_of_lt hj) hcell)]

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
f : α → Fin n
⊢ (Primrec fun a ↦ ↑(f a)) ↔ Primrec f

Tactic:
let : Primcodable { a // a < n } := Primcodable.subtype (nat_lt.comp .id (const _))

Goal state after:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
f : α → Fin n
this : Primcodable { a // a < n } := Primcodable.subtype ⋯
⊢ (Primrec fun a ↦ ↑(f a)) ↔ Primrec f
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case succ.refine_2
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)
⊢ b ∈ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ h a (n + 1 - 1)) (n + 1)

Tactic:
have : ∀ m, (Nat.rec (motive := fun _ => Part σ)
            (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom := by
          intro m
          induction m <;> simp [*, H.fst]
        exact ⟨⟨this n, H.fst⟩, H.snd⟩

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
inst✝ : DecidableRel R
⊢ Primrec₂ fun L b ↦ filter (fun a ↦ decide (R a b)) L

Tactic:
simp only [← List.filterMap_eq_filter]
  refine listFilterMap fst (Primrec.ite ?_ ?_ (Primrec.const Option.none))
  · exact Primrec.eq.comp (hf.decide.comp snd (snd.comp fst)) (.const true)
  · exact option_some.comp snd

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

Goal state before:
pp: case prec
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Primrec' f
a✝ : Primrec' g
hf : Primrec f
hg : Primrec g
⊢ Primrec fun v ↦ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head

Tactic:
| @prec n f g _ _ hf hg =>

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 : ℕ) in atTop, ∀ (i : α), 0 < log (b i * ↑n)

Tactic:
by
  rw [Filter.eventually_all]
  intro i
  have h : Tendsto (fun (n : ℕ) => log (b i * n)) atTop atTop :=
    Tendsto.comp tendsto_log_atTop
      <| Tendsto.const_mul_atTop (b_pos R i) tendsto_natCast_atTop_atTop
  exact h.eventually_gt_atTop 0

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
⊢ x / x₀ ≤ 2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊)

Tactic:
refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_

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
⊢ logb 2 (x / x₀) ≤ logb 2 (2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inl.inr
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
hmain : (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ -|f x| * |g x|
⊢ GrowsPolynomially fun x ↦ -(|f x| * |g x|)

Tactic:
exact this.neg

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

Goal state before:
pp: case inr.inl
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
hmain : (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ -|f x| * |g x|
⊢ GrowsPolynomially fun x ↦ -(|f x| * |g x|)

Tactic:
exact this.neg

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

Goal state before:

Tactic:
(fun (n : ℕ) => q (b i * n) - q (r i n))
      _ ≤ᶠ[atTop] fun (n : ℕ) => ‖q (r i n) - q (b i * n)‖ := by
        filter_upwards with _; rw [norm_sub_rev]; exact le_norm_self _
      _ ≤ᶠ[atTop] fun (n : ℕ) => ‖(b i) ^ (p a b) * n ^ (p a b) * (ε (b i * n) - ε n)‖ :=
        h_main_norm
      _ =ᶠ[atTop] fun (n : ℕ) => (b i) ^ (p a b) * n ^ (p a b) * (ε (b i * n) - ε n) := by
        filter_upwards [eventually_gt_atTop ⌈(b i)⁻¹⌉₊, eventually_gt_atTop 1] with n hn hn'
        refine norm_of_nonneg ?_
        have h₁ := R.b_pos i
        have h₂ : 0 ≤ ε (b i * n) - ε n := by
          refine sub_nonneg_of_le <|
            (strictAntiOn_smoothingFn.le_iff_ge ?n_gt_one ?bn_gt_one).mpr ?le
          case n_gt_one =>
            change 1 < (n : ℝ)
            rw [Nat.one_lt_cast]
            exact hn'
          case bn_gt_one =>
            calc 1 = b i * (b i)⁻¹ := by rw [mul_inv_cancel₀ (by positivity)]
                _ ≤ b i * ⌈(b i)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
                _ < b i * n := by gcongr
          case le => calc b i * n
            _ ≤ 1 * n := by have := R.b_lt_one i; gcongr
            _ = n := by rw [one_mul]
        positivity

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
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) 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
i : α
⊢ ↑n₀ ≤ b' * ↑n

Tactic:
have : (n₀ : ℝ) / b' ≤ n := by
                  exact_mod_cast calc
                    (n₀ : ℝ) / b' ≤ ⌈n₀ / b'⌉₊ := Nat.le_ceil (↑n₀ / b')
                    _ ≤ n := by exact_mod_cast n₀_div_le_n
                rwa [div_le_iff₀, mul_comm] at this
                grind only

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, 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₂ * g ↑n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g ↑n

Tactic:
by gcongr; exact le_max_left _ _

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
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
i : α
⊢ ↑n₀ ≤ b' * ↑n

Tactic:
have : (n₀ : ℝ) / b' ≤ n := by
                  exact_mod_cast calc
                    (n₀ : ℝ) / b' ≤ ⌈n₀ / b'⌉₊ := Nat.le_ceil (↑n₀ / b')
                    _ ≤ n := by exact_mod_cast n₀_div_le_n
                rwa [div_le_iff₀, mul_comm] at this
                grind only

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 : m * l ≤ m
⊢ ⨆ i, m * l ^ i ≤ m

Tactic:
refine iSup_le fun n ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
n : ℕ
⊢ m * l ^ n ≤ m
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
⊢ ⨆ i, l ^ i * m ≤ m

Tactic:
refine iSup_le fun n ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
⊢ l ^ n * m ≤ m
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l m : Language α
⊢ image2 (fun a b ↦ b.reverse ++ a.reverse) l m = image2 (fun a b ↦ a.reverse ++ b.reverse) m l

Tactic:
apply image2_swap

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

Goal state before:
pp: case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
hmain : (fun x ↦ (f x)⁻¹) =ᶠ[atTop] fun x ↦ -|(f x)⁻¹|
⊢ GrowsPolynomially fun x ↦ -|(f x)⁻¹|

Tactic:
exact this.neg

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

Goal state before:
pp: case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ GrowsPolynomially fun x ↦ |(f x)⁻¹|

Tactic:
have hf' : ∀ᶠ x in atTop, f x ≠ 0 := by
      cases hf_pos_or_neg with
      | inl H => filter_upwards [H] with _ hx; exact (ne_of_lt hx).symm
      | inr H => filter_upwards [H] with _ hx; exact (ne_of_gt hx).symm

Goal state after:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
⊢ GrowsPolynomially fun x ↦ |(f x)⁻¹|
Module: Mathlib.Computability.DFA

Goal state before:
pp: case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
⊢ {a} * {b}∗ * {c} ≤ M.accepts

Tactic:
intro y hy

Goal state after:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
y : List α
hy : y ∈ {a} * {b}∗ * {c}
⊢ y ∈ M.accepts
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
⊢ Tendsto (fun n ↦ 1 - ε ↑n) atTop (𝓝 1)

Tactic:
← Function.comp_def (fun n => 1 - ε n) Nat.cast

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto ((fun n ↦ 1 - ε n) ∘ Nat.cast) atTop (𝓝 1)