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

Goal state before:
pp: n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ (ofNatCode (n + 4)).encodeCode = bit n.bodd (bit n.div2.bodd n.div2.div2) + 4

Tactic:
simp only [ofNatCode.eq_5]

Goal state after:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ (match n.bodd, n.div2.bodd with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind').encodeCode =
    bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)

Tactic:
calc 2 * 3
      _ ≤ 2 * 2 ^ 3 := by simp
      _ ≤ 2 * 2 ^ (n + 3) := by gcongr <;> lia

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

Goal state before:
pp: f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, f u ≤ c * f ↑n

Tactic:
by
  obtain ⟨c, hc_mem, hc⟩ := hf.eventually_atTop_le hb
  exact ⟨c, hc_mem, hc.natCast_atTop⟩

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

Goal state before:

Tactic:
(fun (n : ℕ) => (n : ℝ) / log n ^ 2)
    _ = fun (n : ℕ) => (n : ℝ) * ((log n) ^ 2)⁻¹ := by simp_rw [div_eq_mul_inv]
    _ =o[atTop] fun (n : ℕ) => (n : ℝ) * 1⁻¹ := by
      refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_
      refine IsLittleO.inv_rev ?_ (by simp)
      calc
        _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2)) := by simp
        _ =o[atTop] (fun (n : ℕ) => (log n) ^ 2) :=
          IsLittleO.pow (IsLittleO.natCast_atTop <| isLittleO_const_log_atTop) (by norm_num)
    _ = (fun (n : ℕ) => (n : ℝ)) := by ext; simp

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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
i : α
hn : ↑n / log ↑n ^ 2 ≤ (1 - b (max_bi b)) / 2 * ↑n
⊢ ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2

Tactic:
exact hn' i

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 ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n

Tactic:
by
  let c := b (max_bi b) + (1 - b (max_bi b)) / 2
  have h_max_bi_pos : 0 < b (max_bi b) := R.b_pos _
  have h_max_bi_lt_one : 0 < 1 - b (max_bi b) := by
    have : b (max_bi b) < 1 := R.b_lt_one _
    linarith
  have hc_pos : 0 < c := by positivity
  have h₁ : 0 < (1 - b (max_bi b)) / 2 := by positivity
  have hc_lt_one : c < 1 :=
    calc b (max_bi b) + (1 - b (max_bi b)) / 2
      _ = b (max_bi b) * (1 / 2) + 1 / 2 := by ring
      _ < 1 * (1 / 2) + 1 / 2 := by gcongr; exact R.b_lt_one _
      _ = 1 := by norm_num
  refine ⟨c, ⟨hc_pos, hc_lt_one⟩, ?_⟩
  have hlo := isLittleO_self_div_log_id
  rw [Asymptotics.isLittleO_iff] at hlo
  have hlo' := hlo h₁
  filter_upwards [hlo', R.eventually_r_le_b] with n hn hn'
  intro i
  rw [Real.norm_of_nonneg (by positivity)] at hn
  simp only [Real.norm_of_nonneg (by positivity : 0 ≤ (n : ℝ))] at hn
  calc r i n ≤ b i * n + n / log n ^ 2 := by exact hn' i
             _ ≤ b i * n + (1 - b (max_bi b)) / 2 * n := by gcongr
             _ = (b i + (1 - b (max_bi b)) / 2) * n := by ring
             _ ≤ (b (max_bi b) + (1 - b (max_bi b)) / 2) * n := by gcongr; exact max_bi_le _

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

Goal state before:
pp: ⊢ StrictMonoOn (fun x ↦ 1 - ε x) (Set.Ioi 1)

Tactic:
by
  simp_rw [sub_eq_add_neg]
  exact StrictMonoOn.const_add (StrictAntiOn.neg <| strictAntiOn_smoothingFn) 1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (fun n ↦ -log (b i) / ((log (b i) + log ↑n) * log ↑n)) ~[atTop] fun n ↦ -log (b i) / (log ↑n * log ↑n)

Tactic:
refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (fun n ↦ log (b i) + log ↑n) ~[atTop] fun n ↦ log ↑n
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

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

Tactic:
exact le_norm_self _

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

Goal state before:
pp: case hdb
α : 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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑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
this : 0 < u
⊢ ↑n ^ (p a b + 1) ≤ ↑u ^ (p a b + 1)

Tactic:
exact rpow_le_rpow_of_nonpos (by positivity)
          (by exact_mod_cast (le_of_lt hu.2)) (le_of_lt hp)

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
⊢ (map id) l = l

Tactic:
by simp [map]

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ l ^ n * m ≤ m

Tactic:
ih

Goal state after:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ m ≤ m
Module: Mathlib.Computability.Language

Goal state before:
pp: case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ ⨆ i, m ^ i * n ≤ l

Tactic:
iSup_le_iff

Goal state after:
case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ ∀ (i : ℕ), m ^ i * n ≤ l
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.succ
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n✝ : ℕ
ih : m ^ n✝ * n ≤ l
⊢ m * (m ^ n✝ * n) ≤ m * l + n

Tactic:
ih

Goal state after:
case a.succ
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n✝ : ℕ
ih : m ^ n✝ * n ≤ l
⊢ m * l ≤ m * l + n
Module: Mathlib.Computability.DFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : (∀ y ∈ S, y ∈ {x}) → M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, y ∈ {x}
ha : a ∈ {x}
⊢ M.evalFrom s (a :: S).flatten = s

Tactic:
rw [Set.mem_singleton_iff] at ha

Goal state after:
case cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : (∀ y ∈ S, y ∈ {x}) → M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, y ∈ {x}
ha : a = x
⊢ M.evalFrom s (a :: S).flatten = s
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : f false true = true
h✝ : f false false = true
⊢ 2 * n = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : f false true = true
h✝ : ¬f false false = true
⊢ 2 * n = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : ¬f false true = true
h✝ : f false false = true
⊢ False

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : ¬f false true = true
h✝ : ¬f false false = true
⊢ 0 = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : f true false = true
h✝ : f false false = true
⊢ 2 * m = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : f true false = true
h✝ : ¬f false false = true
⊢ 2 * m = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : ¬f true false = true
h✝ : f false false = true
⊢ False

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : ¬f true false = true
h✝ : ¬f false false = true
⊢ 0 = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : ¬m = 0
h✝¹ : ¬n = 0
h✝ : f false false = true
⊢ bitwise f m n + bitwise f m n + 1 = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : ¬m = 0
h✝¹ : ¬n = 0
h✝ : ¬f false false = true
⊢ bitwise f m n + bitwise f m n = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : m = 0
h✝ : f false true = true
⊢ 2 * n + 1 = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : m = 0
h✝ : ¬f false true = true
⊢ 0 = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬m = 0
h✝ : f false true = true
⊢ bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) + 1 = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬m = 0
h✝ : ¬f false true = true
⊢ bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : n = 0
h✝ : f true false = true
⊢ 2 * m + 1 = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : n = 0
h✝ : ¬f true false = true
⊢ 0 = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬n = 0
h✝ : f true false = true
⊢ bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n + 1 = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬n = 0
h✝ : ¬f true false = true
⊢ bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝ : f true true = true
⊢ bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1 =
    2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝ : ¬f true true = true
⊢ bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

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

Goal state before:
pp: case inl
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
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun x ↦ f x ^ p) x) (c₂ * (fun x ↦ f x ^ p) x)

Tactic:
| inl =>

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 : bit yb y ≠ 0
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
⊢ bit (f xb yb) (bitwise f x y) =
    bit (f xb yb)
      (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)

Tactic:
ih

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

Goal state before:
pp: case bit.zero
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
i : ℕ
hn : (bit b n).testBit i = false
hm : testBit 0 i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = testBit 0 j
⊢ bit b n < 0

Tactic:
exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))

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

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ (match 0 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
← xor_one_of_even <| even_iff.mpr ?_,

Goal state after:
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ (match 0 with
      | 0 => n
      | 1 => 1
      | 2 => n ^^^ 1
      | 3 => 0) ^^^
      (n ^^^ 1) =
    match Fin.ofNat 4 1 with
    | 0 => n ^^^ 1
    | 1 => 1
    | 2 => (n ^^^ 1) + 1
    | 3 => 0

n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ n % 2 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ p.bit0.succ.bit0 = p.bit1.bit0

Tactic:
succ

Goal state after:
p : PosNum
⊢ p.bit1.bit0 = p.bit1.bit0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ n.bit0.succ = n.bit1

Tactic:
succ

Goal state after:
n : PosNum
⊢ n.bit1 = n.bit1
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l✝ : List α
a✝ : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l✝ ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l✝
s : σ
⊢ (∃ t ∈ M.evalFrom S l✝, s ∈ M.εClosure (M.step t (some a✝))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l✝, s ∈ M.εClosure (M.step t_1 (some a✝))

Tactic:
ih

Goal state after:
case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l✝ : List α
a✝ : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l✝ ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l✝
s : σ
⊢ (∃ t, (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l✝) ∧ s ∈ M.εClosure (M.step t (some a✝))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l✝, s ∈ M.εClosure (M.step t_1 (some a✝))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' (n + 1)) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1

Tactic:
ih

Goal state after:
case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' n + 1) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ↑↑0 = 0

Tactic:
by rw [Nat.cast_zero, cast_zero]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left✝¹ : x'.reduceOption = x
n : ℕ
t : σ
left✝ : M.IsPath s₁ t x'
u : σ
a✝¹ : u ∈ M.step t (some a)
a✝ : M.IsPath u s₂ (List.replicate n none)
⊢ t ∈ M.evalFrom {s₁} x ∧ ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}

Tactic:
ih

Goal state after:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left✝¹ : x'.reduceOption = x
n : ℕ
t : σ
left✝ : M.IsPath s₁ t x'
u : σ
a✝¹ : u ∈ M.step t (some a)
a✝ : M.IsPath u s₂ (List.replicate n none)
⊢ (∃ x', x'.reduceOption = x ∧ M.IsPath s₁ t x') ∧ ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case prec
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
f✝ h✝ : ℕ →. ℕ
hf✝ : Nat.RecursiveIn O f✝
hh✝ : Nat.RecursiveIn O h✝
ihf : Nat.RecursiveIn O' f✝
ihg : Nat.RecursiveIn O' h✝
⊢ Nat.RecursiveIn O' fun p ↦
    match unpair p with
    | (a, n) =>
      Nat.rec (f✝ a)
        (fun y IH ↦ do
          let i ← IH
          h✝ (Nat.pair a (Nat.pair y i)))
        n

Tactic:
| prec _ _ ihf ihg =>

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case pos
α : 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
⊢ (P.deriv a * Q).rmatch x = true ∨ (Q.deriv a).rmatch x = true ↔
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
ih

Goal state after:
case pos
α : 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
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true ↔
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some.some.goto.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
l : Γ → σ → Λ
h₂ : some (TM1.Stmt.goto l) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.goto l)
⊢ some (M (l a v')) ∈ TM1.stmts M S

Tactic:
exact Finset.some_mem_insertNone.2 (Finset.mem_biUnion.2 ⟨_, hs _ _, TM1.stmts₁_self⟩)

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg
α : 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
⊢ (P.deriv a * Q).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
ih

Goal state after:
case neg
α : 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
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ↔
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ map f (P ^ 0) = map f P ^ 0

Tactic:
unfold map

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ (match P ^ 0 with
    | zero => 0
    | epsilon => 1
    | char a => char (f a)
    | R.plus S => map f R + map f S
    | R.comp S => map f R * map f S
    | R.star => (map f R).star) =
    (match P with
      | zero => 0
      | epsilon => 1
      | char a => char (f a)
      | R.plus S => map f R + map f S
      | R.comp S => map f R * map f S
      | R.star => (map f R).star) ^
      0