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

Goal state before:
pp: case hbc
α : 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 : α
a✝ : i ∈ univ
⊢ ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, 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
x : ℕ
x✝ : x ∈ Ico (r i n) n
⊢ c₂ * g ↑n / ↑n ^ (p a b + 1) ≤ c₂ * g ↑n / ↑n ^ (p a b + 1)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, 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
⊢ sumTransform (p a b) g (r i n) n = ↑n ^ p a b * ∑ u ∈ Ico (r i n) n, g ↑u / ↑u ^ (p a b + 1)

Tactic:
rfl

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
⊢ x ∈ evaln (k₂ + 1) c n

Tactic:
by
    have hl' := Nat.le_of_succ_le_succ hl
    have :
      ∀ {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₂ } := by
      simp only [Option.mem_def, bind, Option.bind_eq_some_iff, Option.guard_eq_some',
        exists_and_left, exists_const, and_imp]
      introv h h₁ h₂ h₃
      exact ⟨le_trans h₂ h, h₁ h₃⟩
    simp? at h ⊢ says simp only [Option.mem_def] at h ⊢
    induction c generalizing x n <;> rw [evaln] at h ⊢ <;> refine this hl' (fun h => ?_) h
    iterate 4 exact h
    case pair cf cg hf hg _ =>
      simp? [Seq.seq, Option.bind_eq_some_iff] at h ⊢ says
        simp only [Seq.seq, Option.map_eq_map, Option.mem_def, Option.bind_eq_some_iff,
          Option.map_eq_some_iff, exists_exists_and_eq_and] at h ⊢
      exact h.imp fun a => And.imp (hf _ _) <| Exists.imp fun b => And.imp_left (hg _ _)
    case comp cf cg hf hg _ =>
      simp? [Bind.bind, Option.bind_eq_some_iff] at h ⊢ says
        simp only [bind, Option.mem_def, Option.bind_eq_some_iff] at h ⊢
      exact h.imp fun a => And.imp (hg _ _) (hf _ _)
    case prec cf cg hf hg _ =>
      revert h
      simp only [unpaired, bind, Option.mem_def]
      induction n.unpair.2 <;> simp [Option.bind_eq_some_iff]
      · apply hf
      · exact fun y h₁ h₂ => ⟨y, evaln_mono hl' h₁, hg _ _ h₂⟩
    case rfind' cf hf _ =>
      simp? [Bind.bind, Option.bind_eq_some_iff] at h ⊢ says
        simp only [unpaired, bind, pair_unpair, Option.pure_def, Option.mem_def,
          Option.bind_eq_some_iff] at h ⊢
      refine h.imp fun x => And.imp (hf _ _) ?_
      by_cases x0 : x = 0 <;> simp [x0]
      exact evaln_mono hl'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
i : α
⊢ b' * ↑n ≤ ↑(r i n)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, 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
x : ℕ
x✝ : x ∈ Ico (r i n) n
⊢ c₂ * g ↑n / ↑(r i n) ^ (p a b + 1) ≤ c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)

Tactic:
rfl

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, C * (a i * T (r i n)) + C * g ↑n = ∑ i, a i * (C * T (r i n)) + C * g ↑n

Tactic:
grind

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 : α
a✝ : i ∈ univ
⊢ r i n ∈ Ico n₀ n

Tactic:
grind

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
x : List α
⊢ x ∈ 1 ↔ x = []

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
x : List α
⊢ (∃ L, x = L.flatten ∧ ∀ y ∈ L, y ∈ l) ↔ ∃ i S, x = S.flatten ∧ S.length = i ∧ ∀ y ∈ S, y ∈ l

Tactic:
grind

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
w : List T
⊢ w ∈ g.language ↔ g.Derives [Symbol.nonterminal g.initial] (List.map Symbol.terminal w)

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case refl
T : Type u_1
g : ContextFreeGrammar T
v w p : List (Symbol T g.NT)
⊢ g.Derives (p ++ v) (p ++ v)

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case refl
T : Type u_1
g : ContextFreeGrammar T
v w p : List (Symbol T g.NT)
⊢ g.Derives (v ++ p) (v ++ p)

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case refl
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ g.reverse.Derives u.reverse u.reverse

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
s : σ
x : List α
⊢ x ∈ M.acceptsFrom s ↔ M.evalFrom s x ∈ M.accept

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts ↔ M.eval x ∈ M.accept

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ M.evalFrom s (List.take (↑n) (List.take (↑m) x)) = M.evalFrom s (List.take (↑n) (List.take (↑m) x))

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    M.evalFrom s (List.take (↑n) (List.take (↑m) x))
⊢ M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t

Tactic:
← hq,

Goal state after:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    M.evalFrom s (List.take (↑n) (List.take (↑m) x))
⊢ M.evalFrom (M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)))
      (List.drop (↑m) x) =
    t
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
⊢ 1 + ε ↑n < 2

Tactic:
grind

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
hS : ∀ y ∈ [], y ∈ {x}
⊢ M.evalFrom s [].flatten = s

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
⊢ (comap f M).accepts = List.map f ⁻¹' M.accepts

Tactic:
by
  ext x
  conv =>
    rhs
    rw [Set.mem_preimage, mem_accepts]
  simp [mem_accepts]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h✝ : f true false = true
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h✝ : ¬f true false = true
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case false
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (false.toNat = 1) = false

Tactic:
rfl

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

Goal state before:
pp: case true
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (true.toNat = 1) = true

Tactic:
rfl

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))) = cast ⋯ (f n.bodd n.div2 (binaryRec z f n.div2))

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg.none
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
e : evaln k c n = Option.none
⊢ (Option.none.bind fun a ↦ evaln k c a) = Option.none

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
⊢ 2 ^ 0 ≤ n ↔ 0 < n

Tactic:
rfl

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

Goal state before:
pp: case false
⊢ (false::zero false) = zero false

Tactic:
rfl

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

Goal state before:
pp: case true
⊢ (true::zero true) = zero true

Tactic:
rfl

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

Goal state before:
pp: case false
⊢ (false::zero (decide ¬false = true)) = nz (msb false)

Tactic:
rfl

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

Goal state before:
pp: case true
⊢ (true::zero (decide ¬true = true)) = nz (msb true)

Tactic:
rfl

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

Goal state before:
pp: case zero
h : ∀ (i : ℕ), testBit 0 i = false
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case zero.false
n : ℕ
⊢ (false.toNat != 0) = false

Tactic:
rfl

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

Goal state before:
pp: case zero.true
n : ℕ
⊢ (true.toNat != 0) = true

Tactic:
rfl

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

Goal state before:
pp: a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i = false ∧ b.testBit i = false ∧ c.testBit i = false
⊢ (false ^^ false ^^ false) = false

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.pair.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
⊢ (Option.none.bind fun a ↦ (evaln k cg n).bind fun y ↦ some (Nat.pair a y)) =
    (Option.map Nat.pair Option.none).bind fun a ↦ Option.map a (evaln (k' + 1) cg n)

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.pair.some.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
val✝ : ℕ
⊢ ((some val✝).bind fun a ↦ Option.none.bind fun y ↦ some (Nat.pair a y)) =
    (Option.map Nat.pair (some val✝)).bind fun a ↦ Option.map a Option.none

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.pair.some.some
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
val✝¹ val✝ : ℕ
⊢ ((some val✝¹).bind fun a ↦ (some val✝).bind fun y ↦ some (Nat.pair a y)) =
    (Option.map Nat.pair (some val✝¹)).bind fun a ↦ Option.map a (some val✝)

Tactic:
rfl

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

Goal state before:
pp: case inl.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
⊢ (true ^^ true) = false

Tactic:
rfl

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

Goal state before:
pp: b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ log x + -1 / 2 * log x ≤ log x + log b

Tactic:
grind

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.comp.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
⊢ (Option.none.bind fun x ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x) =
    Option.none.bind fun x ↦ evaln (k' + 1) cf x

Tactic:
rfl

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

Goal state before:
pp: case inr.inl.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ (true ^^ true) = false

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.prec.zero
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Nat.rec (evaln k cf (unpair n).1)
      (fun n_1 n_ih ↦
        (lup
              (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun i ↦
          lup
            (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      0 =
    Nat.rec (evaln (k' + 1) cf (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      0

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.prec.succ.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ : ℕ
⊢ (Option.none.bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    Option.none.bind fun i ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))

Tactic:
rfl

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

Goal state before:
pp: case inr.inr.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ (true ^^ true) = false

Tactic:
rfl

Goal state after: