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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hodd : Odd (Nat.card V)
⊢ ∅.ncard < (⊤.deleteVerts ∅).coe.oddComponents.ncard

Tactic:
Set.ncard_empty

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hodd : Odd (Nat.card V)
⊢ 0 < (⊤.deleteVerts ∅).coe.oddComponents.ncard
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
⊢ (do
      let n ← Nat.pair <$> Part.some n <*> (↑(decode n)).bind fun a ↦ map encode (f a)
      (↑(decode n)).bind fun a ↦ map encode ((fun p ↦ g p.1 p.2) a)) =
    (↑(decode n)).bind fun a ↦ map encode ((fun a ↦ (f a).bind (g a)) a)

Tactic:
by
    rcases e : decode (α := α) n <;> simp [Seq.seq, e, encodek]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
⊢ (∃ M, M.IsPerfectMatching) → ∀ (u : Set V), ¬G.IsTutteViolator u

Tactic:
by rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM

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

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

Tactic:
simp_rw [isLittleO_neg_left, div_eq_mul_inv]

Goal state after:
p : ℝ
hp : p ≠ 0
⊢ (fun x ↦ x ^ (p - 1) * (log x ^ 2)⁻¹) =o[atTop] fun z ↦ z ^ (p - 1) * 1⁻¹
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)
⊢ R.n₀ ≤ n → 0 < n → 1 < b' * ↑n → ‖q ↑(r i n) - q (b i * ↑n)‖ ≤ c₂ * ‖deriv q ↑n * (↑(r i n) - b i * ↑n)‖

Tactic:
h_ge_n₀

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
⊢ 0 < n → 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:
pp: ⊢ (fun x ↦ (-x * log x ^ 2)⁻¹) =o[atTop] fun x ↦ (x * 1)⁻¹

Tactic:
by
      refine IsLittleO.inv_rev ?_ ?_
      · refine IsBigO.mul_isLittleO
          (by rw [isBigO_neg_right]; aesop (add safe isBigO_refl)) ?_
        rw [isLittleO_one_left_iff]
        exact Tendsto.comp tendsto_norm_atTop_atTop
          <| Tendsto.comp (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
      · exact Filter.Eventually.of_forall (fun x hx => by rw [mul_one] at hx; simp [hx])

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

Goal state before:
pp: ⊢ -deriv ε =ᶠ[atTop] fun x ↦ x⁻¹ / log x ^ 2

Tactic:
by
      filter_upwards with x
      simp [deriv_smoothingFn, neg_div]

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

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 + ε x) x = deriv ε x

Tactic:
rw [deriv_fun_add] <;> aesop

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
i : α
⊢ (fun n ↦ 1 / log (b i * ↑n) - 1 / log ↑n) =ᶠ[atTop] fun n ↦ (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n)

Tactic:
filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * ↑n)
⊢ 1 / log (b i * ↑n) - 1 / log ↑n = (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu✝ : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
⊢ f x ≤ 0

Tactic:
have hu' : (c₁ - c₂) * f x ≤ 0 := by linarith

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu✝ : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
hu' : (c₁ - c₂) * f x ≤ 0
⊢ f x ≤ 0
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
⊢ ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)

Tactic:
change q (r i n) ≤ (b i) ^ (p a b) * n ^ (p a b) * (1 - ε n)

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
⊢ q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
⊢ (fun x ↦ x ^ p a b * x⁻¹) =ᶠ[atTop] fun x ↦ x ^ (p a b - 1)

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx
              rw [← Real.rpow_neg_one, ← Real.rpow_add hx, ← sub_eq_add_neg]

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

Goal state before:
pp: case inr.inr
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, g x ≤ 0
⊢ GrowsPolynomially fun x ↦ f x * g x

Tactic:
have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain]
        exact this

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

Goal state before:
pp: case h₁
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially 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, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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)
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|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ |f u| ≤ c₂ * |f x|

Tactic:
exact (hf u hu).2

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

Goal state before:
pp: case h₁
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
⊢ f u ≤ c₂ * f x

Tactic:
exact (hf u hu).2

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Language α
⊢ (map f) l∗ = ((map f) l)∗

Tactic:
rw [kstar_eq_iSup_pow, kstar_eq_iSup_pow]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
l : Language α
⊢ (map f) (⨆ i, l ^ i) = ⨆ i, (map f) l ^ i
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
H : ∀ᶠ (x : ℝ) in atTop, 0 < f x
a✝ : ℝ
hx : 0 < f a✝
⊢ f a✝ ≠ 0

Tactic:
exact (ne_of_lt hx).symm

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

Goal state before:
pp: C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
h : n ≠ 0
⊢ cast ⋯ (f (1 &&& n != 0) (n >>> 1) (binaryRec z f (n >>> 1))) = ⋯ ▸ f n.bodd n.div2 (binaryRec z f n.div2)

Tactic:
eqRec_eq_cast

Goal state after:
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
h : n ≠ 0
⊢ cast ⋯ (f (1 &&& n != 0) (n >>> 1) (binaryRec z f (n >>> 1))) = cast ⋯ (f n.bodd n.div2 (binaryRec z f n.div2))
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case bit.zero
b : Bool
m : ℕ
e : bit b m ≠ 0
IH : ∀ {n : ℕ}, m < 2 ^ n → m.size ≤ n
h : bit b m < 2 ^ 0
⊢ m.size.succ ≤ 0

Tactic:
exact (e (Nat.lt_one_iff.mp h)).elim

Goal state after:
Module: Mathlib.Data.Num.Basic

Goal state before:
pp: a b : PosNum
⊢ Decidable (a < b)

Tactic:
by dsimp [LT.lt]; infer_instance

Goal state after:
Module: Mathlib.Data.Num.Basic

Goal state before:
pp: a b : Num
⊢ Decidable (a < b)

Tactic:
by dsimp [LT.lt]; infer_instance

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

Goal state before:
pp: case lb
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
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ c₁ ^ p * f x ^ p ≤ f u ^ p

pp: case ub
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
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ^ p ≤ c₂ ^ p * f x ^ p

Tactic:
case lb => calc
      c₁ ^ p * (f x) ^ p = (c₁ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₁_mem) hf_nonneg]
        _ ≤ _ := by gcongr; exact (hf₁ u hu).1

Goal state after:
case ub
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
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ^ p ≤ c₂ ^ p * f x ^ p
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case bit.bit
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap f) m n = bitwise f n m
bn : Bool
n : ℕ
hn : n = 0 → bn = true
a✝ : bitwise (swap f) (bit bm m) n = bitwise f n (bit bm m)
⊢ bitwise (swap f) (bit bm m) (bit bn n) = bitwise f (bit bn n) (bit bm m)

Tactic:
| bit bn n hn =>

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
x : α
l : List (Option α)
⊢ (some x :: l).reduceOption = x :: l.reduceOption

Tactic:
by
  simp only [reduceOption, filterMap, id]

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w✝ = replicate m none ++ some a :: replicate n none
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
use l₁ ++ replicate m none, replicate n none

Goal state after:
case h
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w✝ = replicate m none ++ some a :: replicate n none
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ (replicate n none).reduceOption = []
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons.none
α : Type u_1
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
⊢ (none :: tl).reduceOption.length = (filter Option.isSome (none :: tl)).length

Tactic:
simp [hl]

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons.some
α : Type u_1
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
val✝ : α
⊢ (some val✝ :: tl).reduceOption.length = (filter Option.isSome (some val✝ :: tl)).length

Tactic:
simp [hl]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ ↑n.size + 1 = n.bit0.natSize

Tactic:
natSize,

Goal state after:
n : PosNum
⊢ ↑n.size + 1 = n.natSize.succ
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ ↑n.size + 1 = n.bit1.natSize

Tactic:
natSize,

Goal state after:
n : PosNum
⊢ ↑n.size + 1 = n.natSize.succ
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a + b + c = a + (b + c)

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])))

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a + b = b + a

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])))

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a * b * c = a * (b * c)

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])))

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), 1 * a = a

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])))

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), a * 1 = a

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])))

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a * b = b * a

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])))

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), a ≤ a

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))])))

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
x : List α
⊢ (∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x') → x ∈ M.accepts

Tactic:
intro ⟨s₁, s₂, x', hs₁, hs₂, h⟩
    have := M.mem_evalFrom_iff_exists.mpr ⟨_, hs₁, M.mem_evalFrom_iff_exists_path.mpr ⟨_, h⟩⟩
    exact ⟨s₂, hs₂, this⟩

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
⊢ M.toεNFA.accepts = M.accepts

Tactic:
rw [εNFA.accepts, εNFA.eval, toεNFA_evalFrom_match]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
⊢ {x | ∃ S ∈ M.toεNFA.accept, S ∈ M.evalFrom M.toεNFA.start x} = M.accepts
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
⊢ L.toDFA.accepts = L

Tactic:
by
  ext x
  rw [DFA.mem_accepts]
  suffices L.toDFA.eval x = L.leftQuotient x by simp [this]
  induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih, leftQuotient_append]

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: case inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : x ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
exact Or.inr ha

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
⊢ ∃ b₁, tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁

Tactic:
rcases tr_reaches_rev H aa ab with ⟨c₁, c₂, bc, cc, ac⟩

Goal state after:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
c₂ : σ₂
bc : Reaches f₂ b₂ c₂
cc : tr c₁ c₂
ac : Reaches f₁ a₁ c₁
⊢ ∃ b₁, tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ Supports M Set.univ

Tactic:
constructor <;> intros

Goal state after:
case left
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ default ∈ Set.univ

case right
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
q✝ : Λ
a✝² : Γ
q'✝ : Λ
s✝ : Stmt Γ
a✝¹ : (q'✝, s✝) ∈ M q✝ a✝²
a✝ : q✝ ∈ Set.univ
⊢ q'✝ ∈ Set.univ
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
⊢ q ∈ stmts₁ q

Tactic:
by
  cases q <;> simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
⊢ q₀ ∈ stmts₁ q₂

Tactic:
induction q₂ with

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
⊢ SupportsStmt S q₁

Tactic:
induction q₂ with

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

Goal state before:
pp: case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k✝ : K
a✝¹ : σ → Γ k✝
a✝ : Stmt Γ Λ σ
⊢ push k✝ a✝¹ a✝ ∈ stmts₁ (push k✝ a✝¹ a✝)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

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

Goal state before:
pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
⊢ peek k✝ a✝¹ a✝ ∈ stmts₁ (peek k✝ a✝¹ a✝)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

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

Goal state before:
pp: case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
⊢ pop k✝ a✝¹ a✝ ∈ stmts₁ (pop k✝ a✝¹ a✝)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

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

Goal state before:
pp: case load
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a✝¹ : σ → σ
a✝ : Stmt Γ Λ σ
⊢ load a✝¹ a✝ ∈ stmts₁ (load a✝¹ a✝)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

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

Goal state before:
pp: case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a✝² : σ → Bool
a✝¹ a✝ : Stmt Γ Λ σ
⊢ branch a✝² a✝¹ a✝ ∈ stmts₁ (branch a✝² a✝¹ a✝)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

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

Goal state before:
pp: case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a✝ : σ → Λ
⊢ goto a✝ ∈ stmts₁ (goto a✝)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

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

Goal state before:
pp: case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
⊢ halt ∈ stmts₁ halt

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

Goal state after: