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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
⊢ (bif (encode (f a)).bodd then Option.map (h a) (decode (encode (f a)).div2)
    else Option.map (g a) (decode (encode (f a)).div2)) =
    Option.some (Sum.casesOn (f a) (g a) (h a))

Tactic:
rcases f a with b | c

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
b : β
⊢ (bif (encode (Sum.inl b)).bodd then Option.map (h a) (decode (encode (Sum.inl b)).div2)
    else Option.map (g a) (decode (encode (Sum.inl b)).div2)) =
    Option.some (Sum.casesOn (Sum.inl b) (g a) (h a))

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
c : γ
⊢ (bif (encode (Sum.inr c)).bodd then Option.map (h a) (decode (encode (Sum.inr c)).div2)
    else Option.map (g a) (decode (encode (Sum.inr c)).div2)) =
    Option.some (Sum.casesOn (Sum.inr c) (g a) (h a))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v ↦ (unpair (f v)).1

Tactic:
have s := sqrt.comp₁ _ hf

Goal state after:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
⊢ Primrec' fun v ↦ (unpair (f v)).1
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v ↦ (unpair (f v)).2

Tactic:
have s := sqrt.comp₁ _ hf

Goal state after:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
⊢ Primrec' fun v ↦ (unpair (f v)).2
Module: Mathlib.Computability.Ackermann

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

Tactic:
by gcongr; exact add_add_one_le_ack ..

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf : Code
⊢ encode cf < encode cf.rfind'

Tactic:
simp only [encodeCode_eq, encodeCode]
  lia

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
C c : ℝ
hc_mem : c ∈ Set.Ioo 0 1
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)
n : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * ↑n ≤ ↑(r i n)
i : α
h₁ : 0 < c
⊢ C = c * (C / c)

Tactic:
rw [← mul_div_assoc]
      exact (mul_div_cancel_left₀ _ (by positivity)).symm

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

Goal state before:

Tactic:
C
    _ = c * (C / c) := by
      rw [← mul_div_assoc]
      exact (mul_div_cancel_left₀ _ (by positivity)).symm
    _ ≤ c * ⌈C / c⌉₊ := by gcongr; simp [Nat.le_ceil]
    _ ≤ c * n := by gcongr
    _ ≤ r i n := hn₂ i

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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
⊢ 1 < x →
    deriv (fun x ↦ x ^ p a b * (1 - ε x)) x =
      deriv (fun z ↦ z ^ p a b) x * (1 - ε x) + x ^ p a b * deriv (fun z ↦ 1 - ε z) x

Tactic:
hx'

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)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ deriv (fun x ↦ x ^ p a b * (1 - ε x)) x =
    deriv (fun z ↦ z ^ p a b) x * (1 - ε x) + x ^ p a b * deriv (fun z ↦ 1 - ε z) x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (fun x ↦ -x⁻¹ / log x ^ 2) = fun x ↦ (-x * log x ^ 2)⁻¹

Tactic:
neg_div,

Goal state after:
⊢ (fun x ↦ -(x⁻¹ / log x ^ 2)) = fun x ↦ (-x * log x ^ 2)⁻¹
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:
by
          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: f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∃ᶠ (x : ℝ) in atTop, f x = 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x = 0

Tactic:
obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf (1 / 2) (by norm_num)
  rw [frequently_atTop] at hf'
  filter_upwards [eventually_forall_ge_atTop.mpr hf, eventually_gt_atTop 0] with x hx hx_pos
  obtain ⟨x₀, hx₀_ge, hx₀⟩ := hf' (max x 1)
  have x₀_pos := calc
    0 < 1 := by norm_num
    _ ≤ x₀ := le_of_max_le_right hx₀_ge
  have hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z →
      z ∈ Set.Icc ((2 : ℝ) ^ (-(m : ℤ) - 1) * x₀) ((2 : ℝ) ^ (-(m : ℤ)) * x₀) → f z = 0 := by
    intro m
    induction m with
    | zero =>
      simp only [CharP.cast_eq_zero, neg_zero, zero_sub, zpow_zero, one_mul] at *
      specialize hx x₀ (le_of_max_le_left hx₀_ge)
      simp only [hx₀, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
      refine fun z _ hz => hx _ ?_
      simp only [zpow_neg, zpow_one] at hz
      simp only [one_div, hz]
    | succ k ih =>
      intro z hxz hz
      simp only [Nat.cast_add, Nat.cast_one] at *
      have hx' : x ≤ (2 : ℝ) ^ (-(k : ℤ) - 1) * x₀ := by
        calc x ≤ z := hxz
          _ ≤ _ := by simp only [neg_add, ← sub_eq_add_neg] at hz; exact hz.2
      specialize hx ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' z
      specialize ih ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' ?ineq
      case ineq =>
        rw [Set.left_mem_Icc]
        gcongr
        · norm_num
        · lia
      simp only [ih, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
      refine hx ⟨?lb₁, ?ub₁⟩
      case lb₁ =>
        rw [one_div, ← zpow_neg_one, ← mul_assoc, ← zpow_add₀ (by norm_num)]
        have h₁ : (-1 : ℤ) + (-k - 1) = -k - 2 := by ring
        have h₂ : -(k + (1 : ℤ)) - 1 = -k - 2 := by ring
        rw [h₁]
        rw [h₂] at hz
        exact hz.1
      case ub₁ =>
        have := hz.2
        simp only [neg_add, ← sub_eq_add_neg] at this
        exact this
  refine hmain ⌊-logb 2 (x / x₀)⌋₊ x le_rfl ⟨?lb, ?ub⟩
  case lb =>
    rw [← le_div_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (zpow_pos (by norm_num) _)
      (by positivity)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_sub, Int.cast_neg, Int.cast_natCast, Int.cast_one, neg_sub, sub_neg_eq_add]
    calc -logb 2 (x / x₀) ≤ ⌈-logb 2 (x / x₀)⌉₊ := Nat.le_ceil (-logb 2 (x / x₀))
         _ ≤ _ := by rw [add_comm]; exact_mod_cast Nat.ceil_le_floor_add_one _
  case ub =>
    rw [← div_le_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_neg, Int.cast_natCast, neg_neg]
    have : 0 ≤ -logb 2 (x / x₀) := by
      rw [neg_nonneg]
      refine logb_nonpos (by norm_num) (by positivity) ?_
      rw [div_le_one x₀_pos]
      exact le_of_max_le_left hx₀_ge
    exact_mod_cast Nat.floor_le this

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
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)
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / log ↑n ^ 2

Tactic:
have hn' : (n : ℝ) ≠ 0 := by positivity

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)
n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / log ↑n ^ 2
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
⊢ 1 < x → 0 < 1 + ε x

Tactic:
hx'

Goal state after:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
⊢ 0 < 1 + ε x
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)
x : ℝ
hx : x ≠ 0
⊢ 1 < x →
    deriv (fun x ↦ x ^ p a b * (1 + ε x)) x =
      deriv (fun z ↦ z ^ p a b) x * (1 + ε x) + x ^ p a b * deriv (fun z ↦ 1 + ε z) x

Tactic:
hx'

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)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ deriv (fun x ↦ x ^ p a b * (1 + ε x)) x =
    deriv (fun z ↦ z ^ p a b) x * (1 + ε x) + x ^ p a b * deriv (fun z ↦ 1 + ε z) x
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)
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / log ↑n ^ 2

Tactic:
have hn' : (n : ℝ) ≠ 0 := by positivity

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)
n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / log ↑n ^ 2
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: 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)
⊢ c₂ * c₄ > 0

Tactic:
change 0 < c₂ * c₄

Goal state after:
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)
⊢ 0 < c₂ * c₄
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c₁ c₂ : Code
n₁ n₂ : ℕ
h : c₁.curry n₁ = c₂.curry n₂
⊢ n₁ = n₂

Tactic:
injection h with h₁ h₂
    injection h₂ with h₃ h₄
    exact const_inj h₃

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'.succ
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
⊢ ∃ k,
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ a,
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
| succ y IH =>

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.h
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n✝ : ℕ
ih : ∀ m_1 < n✝, ∀ ⦃x : List α⦄, x ∈ l → x.length = m_1 → x ∈ m∗ * n
x : List α
hx : x ∈ l
hlen : x.length = n✝
⊢ x ∈ m∗ * n

Tactic:
| _ _ ih
       => 

Goal state after:
case a.h
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n✝ : ℕ
ih : ∀ m_1 < n✝, ∀ ⦃x : List α⦄, x ∈ l → x.length = m_1 → x ∈ m∗ * n
x : List α
hx : x ∈ l
hlen : x.length = n✝
⊢ x ∈ m∗ * n
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.h.inl
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : ∀ m_1 < (a ++ b).length, ∀ ⦃x : List α⦄, x ∈ l → x.length = m_1 → x ∈ m∗ * n
hx : a ++ b ∈ m * l
⊢ a ++ b ∈ m∗ * n

Tactic:
rw [length_append] at ih

Goal state after:
case a.h.inl
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : ∀ m_1 < a.length + b.length, ∀ ⦃x : List α⦄, x ∈ l → x.length = m_1 → x ∈ m∗ * n
hx : a ++ b ∈ m * l
⊢ a ++ b ∈ m∗ * n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case f
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
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ
| (lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1) p.1.1.1.2).bind fun y ↦ some (Nat.pair p.2 y)

Tactic:
← Option.map_eq_bind

Goal state after:
case f
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
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ
| Option.map (Nat.pair p.2) (lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1) p.1.1.1.2)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
x : ℝ
hx : f x = 0
⊢ (∀ (y : ℝ), b * id x ≤ y → f y = 0) → ∀ u ∈ Set.Icc (b * x) x, (f u)⁻¹ ∈ Set.Icc (1 * (f x)⁻¹) (1 * (f x)⁻¹)

Tactic:
hx'

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
x : ℝ
hx : f x = 0
hx' : ∀ (y : ℝ), b * id x ≤ y → f y = 0
⊢ ∀ u ∈ Set.Icc (b * x) x, (f u)⁻¹ ∈ Set.Icc (1 * (f x)⁻¹) (1 * (f x)⁻¹)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: 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
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
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)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
⊢ f x ≠ 0 →
    (∀ (y : ℝ), b * id x ≤ y → f y ≠ 0) → ∀ u ∈ Set.Icc (b * x) x, |f u|⁻¹ ∈ Set.Icc (c₂⁻¹ * |f x|⁻¹) (c₁⁻¹ * |f x|⁻¹)

Tactic:
hx'

Goal state after:
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
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
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)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
⊢ (∀ (y : ℝ), b * id x ≤ y → f y ≠ 0) → ∀ u ∈ Set.Icc (b * x) x, |f u|⁻¹ ∈ Set.Icc (c₂⁻¹ * |f x|⁻¹) (c₁⁻¹ * |f x|⁻¹)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: 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
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
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)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
⊢ (∀ (y : ℝ), b * id x ≤ y → f y ≠ 0) → ∀ u ∈ Set.Icc (b * x) x, |f u|⁻¹ ∈ Set.Icc (c₂⁻¹ * |f x|⁻¹) (c₁⁻¹ * |f x|⁻¹)

Tactic:
hx''

Goal state after:
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
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
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)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
⊢ ∀ u ∈ Set.Icc (b * x) x, |f u|⁻¹ ∈ Set.Icc (c₂⁻¹ * |f x|⁻¹) (c₁⁻¹ * |f x|⁻¹)
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
x : ℝ
hx : f x = 0
⊢ (∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) →
    ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (1 * f x ^ p) (1 * f x ^ p)

Tactic:
hx'

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 : ℝ
hx : f x = 0
hx' : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (1 * f x ^ p) (1 * f x ^ p)
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
hneg : ∀ᶠ (x : ℝ) in atTop, f x < 0
x : ℝ
hx : 0 ≤ f x
⊢ f x < 0 → False

Tactic:
hx'

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
hneg : ∀ᶠ (x : ℝ) in atTop, f x < 0
x : ℝ
hx : 0 ≤ f x
hx' : f x < 0
⊢ False
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: this :
  Primrec₂ fun x n ↦
    let a := ofNat (ℕ × Code) n;
    List.map (evaln a.1 a.2) (List.range a.1)
x✝ : (ℕ × Code) × ℕ
k : ℕ
c : Code
n : ℕ
⊢ ((let a := ofNat (ℕ × Code) (encode ((k, c), n).1);
          List.map (evaln a.1 a.2) (List.range a.1))[((k, c), n).2]?.bind
      fun b ↦ (((k, c), n), b).2) =
    evaln ((k, c), n).1.1 ((k, c), n).1.2 ((k, c), n).2

Tactic:
by simp [evaln_map, Option.bind_map]

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'
hl₂ : w✝.reduceOption = [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
rw [reduceOption_eq_singleton_iff] at hl₂

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

Goal state before:
pp: b : Bool
n : Num
⊢ ↑(bit b n) = Nat.bit b ↑n

Tactic:
cases b <;> cases n

Goal state after:
case false.zero
⊢ ↑(bit false zero) = Nat.bit false ↑zero

case false.pos
a✝ : PosNum
⊢ ↑(bit false (pos a✝)) = Nat.bit false ↑(pos a✝)

case true.zero
⊢ ↑(bit true zero) = Nat.bit true ↑zero

case true.pos
a✝ : PosNum
⊢ ↑(bit true (pos a✝)) = Nat.bit true ↑(pos a✝)
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₂⁻¹ * c₃ * f x ≤ f u

Tactic:
calc
    c₁ * c₂⁻¹ * c₃ * f x ≤ c₁ * c₂⁻¹ * c₃ * (c₂ * ‖g x‖) := by
          rw [← Real.norm_of_nonneg (hf_pos x hbx)]; gcongr; exact h_ub x hbx
      _ = (c₂⁻¹ * c₂) * c₁ * (c₃ * ‖g x‖) := by ring
      _ = c₁ * (c₃ * ‖g x‖) := by simp [c₂_cancel]
      _ ≤ c₁ * ‖g u‖ := by gcongr; exact (hg_bound u hu).1
      _ ≤ f u := by
          rw [← Real.norm_of_nonneg (hf_pos u hu.1)]
          exact h_lb u hu.1

Goal state after: