mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case neg.inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x ∧ 0 ≠ f x

Tactic:
rw [eventually_and]

Goal state after:
case neg.inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∧ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case neg.inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0 ∧ f x ≠ 0

Tactic:
rw [eventually_and]

Goal state after:
case neg.inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x ≤ 0) ∧ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_2
f : ℕ →. ℕ
⊢ (∃ c, c.eval = f) → Nat.Partrec f

Tactic:
· rintro ⟨c, rfl⟩
    induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
⊢ x ∈ evaln (k₂ + 1) c n

Tactic:
simp? at h ⊢ says simp only [Option.mem_def] at h ⊢

Goal state after:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
h : evaln (k + 1) c n = some x
⊢ evaln (k₂ + 1) c n = some x
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 : u ∈ Ico (r i n) n
⊢ u ≤ n

Tactic:
· rw [Finset.mem_Ico] at hu
          exact le_of_lt hu.2

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

Goal state before:
pp: case bc.a
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
⊢ - -‖g x‖ ≤ -(1 / 2 * f x)

Tactic:
neg_neg,

Goal state after:
case bc.a
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
⊢ ‖g x‖ ≤ -(1 / 2 * f x)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case h₂
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ - -‖g u‖ ≤ -(1 / 2 * f u)

Tactic:
neg_neg,

Goal state after:
case h₂
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ ‖g u‖ ≤ -(1 / 2 * f u)
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
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₂ * f x) ^ p = c₂ ^ p * f x ^ p

Tactic:
by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]

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

Goal state before:
pp: case pos
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
this : n = m
⊢ (fun x ↦ 2 * x) m < (fun x ↦ 2 * x + 1) m

Tactic:
exact Nat.lt_succ_self _

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

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

Tactic:
convert! hnm j.succ (succ_lt_succ hj) using 1

Goal state after:
case e'_2
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ n.testBit j = (bit b n).testBit j.succ

case e'_3
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ m.testBit j = (bit b' m).testBit j.succ
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‖
⊢ (∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)) →
    0 ≤ x → ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)

Tactic:
hg_bound

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‖)
⊢ 0 ≤ x → ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
h : ↑m < ↑n
⊢ ↑m + ↑m + 1 + 1 ≤ ↑n + ↑n

Tactic:
rw [Nat.add_right_comm m m 1, add_assoc]

Goal state after:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m + 1 + (↑m + 1) ≤ ↑n + ↑n
Module: Mathlib.Data.List.ReduceOption

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

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

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

Goal state before:
pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1

Tactic:
· rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
        ofNat'_bit, ofNat'_bit, ih]
      simp only [cond, add_one, bit1_succ]

Goal state after:
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‖)
⊢ ‖f u‖ ≤ c₂ * ‖g u‖

Tactic:
exact h_ub u hu.1

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' fun v ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
⊢ Partrec' f

Tactic:
let g := fun n₁ =>
        (Part.ofOption (decode (α := List.Vector ℕ n) n₁)).bind (fun a => Part.map encode (f a))

Goal state after:
this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' fun v ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
g : ℕ → Part ℕ := fun n₁ ↦ (↑(decode n₁)).bind fun a ↦ Part.map encode (f a)
⊢ Partrec' f
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: f : ℕ → ℕ →. ℕ
h : Partrec fun v ↦ f v.head v.tail.head
v : ℕ × ℕ
⊢ f (v.1 ::ᵥ v.2 ::ᵥ nil).head (v.1 ::ᵥ v.2 ::ᵥ nil).tail.head = f v.1 v.2

Tactic:
by
        simp only [head_cons, tail_cons]

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1.some
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
⊢ Reaches f a b ∧ f b = none

Tactic:
· rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩) <;> rw [e] at h <;>
        cases Part.mem_some_iff.1 h
      obtain ⟨h₁, h₂⟩ := IH a' e
      exact ⟨ReflTransGen.head e h₁, h₂⟩

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
x✝ : Reaches₁ f b c
bc : Reaches₁ f b c := x✝
⊢ False

Tactic:
by
    let ⟨_, b0⟩ := mem_eval.1 h
    let ⟨b', h', _⟩ := TransGen.head'_iff.1 bc
    cases b0.symm.trans h'

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

Goal state before:
pp: Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
⊢ Respects (step M) (step (M.map f₁ f₂ g₁.f g₂)) fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b

Tactic:
by
  intro c _ ⟨cs, rfl⟩
  cases e : step M c
  · rw [← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs, e]
    rfl
  · refine ⟨_, ⟨step_supports M ss e cs, rfl⟩, TransGen.single ?_⟩
    rw [← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs, e]
    rfl

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case pos.mpr.nil
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
h : a :: x = [] ++ u
hP : P.rmatch [] = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true

pp: case pos.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : P.rmatch (b :: t) = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true

Tactic:
· right
          rw [List.nil_append] at h
          rw [← h] at hQ
          exact hQ

Goal state after:
case pos.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : P.rmatch (b :: t) = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
this : ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
⊢ (Tape.move Dir.right)^[n] ((Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons R.head L) R.tail)) =
    (Tape.move Dir.right)^[n] (trTape' enc0 L R)

Tactic:
simp only [trTape'_move_left, ListBlank.cons_head_tail, ListBlank.head_cons,
      ListBlank.tail_cons]

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₁ l₂ : List Bool
f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
    stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
induction l₂ generalizing l₁ with
  | nil => rfl
  | cons a l₂ IH =>
    trans stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
        (Tape.mk' ((L'.append l₁).cons a) (R'.append l₂))
    · dsimp [readAux, stepAux]
      simp only [ListBlank.head_cons, Tape.move_right_mk', ListBlank.tail_cons]
      cases a <;> rfl
    · rw [← ListBlank.append, IH]
      rfl

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

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
m : PosNum
⊢ m.testBit n = (Nat.bit true ↑m).testBit (n + 1)

Tactic:
Nat.testBit_bit_succ,

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
m : PosNum
⊢ m.testBit n = (↑m).testBit n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
m : PosNum
⊢ m.testBit n = (Nat.bit false ↑m).testBit (n + 1)

Tactic:
Nat.testBit_bit_succ,

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
m : PosNum
⊢ m.testBit n = (↑m).testBit n
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
x✝ : ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b
e : ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b := x✝
⊢ Epi (Sigma.desc π)

Tactic:
by
    rw [epi_iff_surjective]
    intro b
    obtain ⟨t, x, h⟩ := e b
    refine ⟨Sigma.ι X t x, ?_⟩
    change (Sigma.ι X t ≫ Sigma.desc π) x = _
    simpa using h

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

Goal state before:
pp: case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
this : Cfg.halt v' ∈ (f.eval v).bind fun v ↦ eval step (Cfg.ret Cont.halt v)
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
Part.mem_bind_iff

Goal state after:
case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
this : ∃ a ∈ f.eval v, Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt a)
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
c₁ : TM2.Cfg Γ Λ σ
c₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h : TrCfg c₁ c₂
⊢ match TM2.step M c₁ with
  | some b₁ => ∃ b₂, TrCfg b₁ b₂ ∧ Reaches₁ (TM1.step (tr M)) c₂ b₂
  | none => TM1.step (tr M) c₂ = none

Tactic:
obtain @⟨- | l, v, S, L, hT⟩ := h

Goal state after:
case none
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ match TM2.step M { l := none, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal none, var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal none, var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

case some
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
⊢ match TM2.step M { l := some l, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } = none
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
⊢ Subtype.val '' range Subtype.val = interior s

Tactic:
Subtype.range_coe,

Goal state after:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
⊢ Subtype.val '' u = interior s