mathlib-initiative/mathlib-tactics huggingface dataset:
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
gt_zero : 0 < b (min_bi b)
hlo : (fun n ↦ ↑n / log ↑n ^ 2) =o[atTop] fun n ↦ ↑n
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)

Tactic:
rw [Asymptotics.isLittleO_iff] at hlo

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

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

Tactic:
by
      refine IsEquivalent.add_isLittleO ?one ?two
      case one => calc
        (fun z => p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1) * 1 :=
              IsEquivalent.mul IsEquivalent.refl isEquivalent_one_add_smoothingFn_one
        _ = fun z => p * z ^ (p - 1) := by ext; ring
      case two => calc
        (fun z => -(z ^ (p - 1) / (log z ^ 2))) =o[atTop] fun z => z ^ (p - 1) / 1 := by
            simp_rw [isLittleO_neg_left, div_eq_mul_inv]
            refine IsBigO.mul_isLittleO (isBigO_refl _ _)
              (IsLittleO.inv_rev ?_ (by simp))
            rw [isLittleO_const_left]
            refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
            exact Tendsto.comp (g := fun z => z ^ 2)
              (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _

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

Goal state before:
pp: case inl
p : ℝ
hp : p = 0
h₁ : (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖) =ᶠ[atTop] fun z ↦ z⁻¹ / log z ^ 2
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ log x

Tactic:
filter_upwards [eventually_ge_atTop 1] with _ hx using log_nonneg hx

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 : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : (fun n ↦ ↑n / log ↑n ^ 2) =o[atTop] fun n ↦ ↑n
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n

Tactic:
rw [Asymptotics.isLittleO_iff] at hlo

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
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₀

Tactic:
exact le_of_max_le_left hx₀_ge

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

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

Tactic:
filter_upwards with x
      simp [deriv_smoothingFn]

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
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁⁻¹
h_ind : ∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ ∑ i, C * (1 - ε ↑n) * (asympBound g a b n - c₁ * g ↑n) * (a i * b i ^ p a b) + g ↑n =
    C * (1 - ε ↑n) * (asympBound g a b n - c₁ * g ↑n) + g ↑n

Tactic:
← Finset.mul_sum,

Goal state after:
α : 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
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁⁻¹
h_ind : ∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ C * (1 - ε ↑n) * (asympBound g a b n - c₁ * g ↑n) * ∑ i, a i * b i ^ p a b + g ↑n =
    C * (1 - ε ↑n) * (asympBound g a b n - c₁ * g ↑n) + g ↑n
Module: Mathlib.Computability.AkraBazzi.SumTransform

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

Tactic:
by exact_mod_cast hu.1

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n x : ℕ
left✝ : n ≤ k
h :
  ∃ a,
    evaln (k + 1) cf n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x

Tactic:
rcases h with ⟨m, h₁, h₂⟩

Goal state after:
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n x : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
h₂ : (if m = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg.succ
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + ((unpair n).2 + 1)))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some (y + ((unpair n).2 + 1))
i : ℕ
im : i + 1 < y + 1
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2)), ¬a = 0

Tactic:
rcases hy₂ (Nat.lt_of_succ_lt_succ im) with ⟨z, hz, z0⟩
          exact ⟨z, by simpa [add_comm, add_left_comm] using hz, z0⟩

Goal state after:
Module: Mathlib.Computability.Language

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

Tactic:
by
  constructor
  · rintro ⟨S, rfl, h⟩
    refine ⟨S.filter fun l ↦ !List.isEmpty l,
      by simp [List.flatten_filter_not_isEmpty], fun y hy ↦ ?_⟩
    simp only [mem_filter, Bool.not_eq_eq_eq_not, Bool.not_true, isEmpty_eq_false_iff, ne_eq] at hy
    exact ⟨h y hy.1, hy.2⟩
  · rintro ⟨S, hx, h⟩
    exact ⟨S, hx, fun y hy ↦ (h y hy).1⟩

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
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ ∑ i, (1 + ε ↑n) * (asympBound g a b n - c₁ * g ↑n) * (a i * b i ^ p a b) + C * g ↑n =
    (1 + ε ↑n) * (asympBound g a b n - c₁ * g ↑n) + C * g ↑n

Tactic:
← Finset.mul_sum,

Goal state after:
α : 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
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ (1 + ε ↑n) * (asympBound g a b n - c₁ * g ↑n) * ∑ i, a i * b i ^ p a b + C * g ↑n =
    (1 + ε ↑n) * (asympBound g a b n - c₁ * g ↑n) + C * g ↑n
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
σ' : Type u_2
f : α' → α
g : σ ≃ σ'
⊢ comap f ((reindex g) M) = (reindex g) (comap f M)

Tactic:
by
  simp [comap, reindex]

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

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
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₂ * f x) ^ p

Tactic:
gcongr; exact (hf₁ u hu).2

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

Goal state before:
pp: case bit.bit
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
        (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x y
yb : Bool
y : ℕ
hyb : y = 0 → yb = true
a✝ :
  bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 ↦
        bit (f xb b)
          (binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
            (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x n))
      y
⊢ bitwise f (bit xb x) (bit yb y) =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 ↦
        bit (f xb b)
          (binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
            (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x n))
      (bit yb y)

Tactic:
| bit yb y hyb =>

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

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false

Tactic:
by
  induction n using Nat.binaryRec with | zero => exact False.elim (h rfl) | bit b n hn => ?_
  by_cases h' : n = 0
  · subst h'
    rw [show b = true by
        revert h
        cases b <;> simp]
    refine ⟨0, ⟨by rw [testBit_bit_zero], fun j hj => ?_⟩⟩
    obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (ne_of_gt hj)
    rw [testBit_bit_succ, zero_testBit]
  · obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'
    refine ⟨k + 1, ⟨by rw [testBit_bit_succ, hk], fun j hj => ?_⟩⟩
    obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (show j ≠ 0 by intro x; subst x; simp at hj)
    exact (testBit_bit_succ _ _ _).trans (hk' _ (lt_of_succ_lt_succ hj))

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

Goal state before:
pp: case inl
n i : ℕ
⊢ (n &&& 2 ^ i).testBit i = ((n.testBit i).toNat * 2 ^ i).testBit i

Tactic:
cases h : n.testBit i

Goal state after:
case inl.false
n i : ℕ
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit i = (false.toNat * 2 ^ i).testBit i

case inl.true
n i : ℕ
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit i = (true.toNat * 2 ^ i).testBit i
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr
n i j : ℕ
hij : i ≠ j
⊢ (n &&& 2 ^ i).testBit j = ((n.testBit i).toNat * 2 ^ i).testBit j

Tactic:
cases h : n.testBit i

Goal state after:
case inr.false
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j

case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j
Module: Mathlib.Computability.Encoding

Goal state before:
pp: n : Num
⊢ decodeNum (encodeNum n) = n

Tactic:
obtain - | n := n

Goal state after:
case zero
⊢ decodeNum (encodeNum Num.zero) = Num.zero

case pos
n : PosNum
⊢ decodeNum (encodeNum (Num.pos n)) = Num.pos n
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons
α : Type u_1
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → x.isSome = true) ↔ none ∈ tail✝
⊢ (¬∀ (x : Option α), x ∈ head✝ :: tail✝ → x.isSome = true) ↔ none ∈ head✝ :: tail✝

Tactic:
· grind [cases Option]

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

Goal state before:
pp: m n : PosNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]

Goal state after:
m n : PosNum
⊢ ¬↑n < ↑m ↔ m ≤ n
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
simp [Nat.bit, mul_add]

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

Goal state before:
pp: m n : Num
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]

Goal state after:
m n : Num
⊢ ¬↑n < ↑m ↔ m ≤ n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : PosNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : PosNum
⊢ ¬↑n < ↑m ↔ m ≤ n
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
x y : List α
⊢ L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y

Tactic:
simp [leftQuotient, Language]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : Num
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : Num
⊢ ¬↑n < ↑m ↔ m ≤ n
Module: Mathlib.Computability.RE

Goal state before:
pp: case inl
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e : x ∈ Code.evaln k cf n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
simp [Code.evaln_sound e]

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: case inr
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e : x ∈ Code.evaln k cg n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
simp [Code.evaln_sound e]

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

Goal state before:
pp: case zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
n : Num
⊢ ↑(f zero n) = Nat.bitwise g ↑zero ↑n

Tactic:
obtain - | n := n

Goal state after:
case zero.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
⊢ ↑(f zero zero) = Nat.bitwise g ↑zero ↑zero

case zero.pos
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
n : PosNum
⊢ ↑(f zero (pos n)) = Nat.bitwise g ↑zero ↑(pos n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
n : Num
m : PosNum
⊢ ↑(f (pos m) n) = Nat.bitwise g ↑(pos m) ↑n

Tactic:
obtain - | n := n

Goal state after:
case pos.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m : PosNum
⊢ ↑(f (pos m) zero) = Nat.bitwise g ↑(pos m) ↑zero

case pos.pos
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m n : PosNum
⊢ ↑(f (pos m) (pos n)) = Nat.bitwise g ↑(pos m) ↑(pos n)
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i : Fin n
⊢ Partrec' (Fin.cases f (fun i v ↦ ↑(some (v.get i))) i.succ)

Tactic:
simpa using! prim (Nat.Primrec'.get i)

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

Goal state before:
pp: case zero.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
⊢ ↑(f 0 0) = Nat.bitwise g 0 0

Tactic:
f00,

Goal state after:
case zero.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
⊢ ↑0 = Nat.bitwise g 0 0