mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ C * (∑ i, a i * T (r i n) + g ↑n) = ∑ i, a i * (C * T (r i n)) + C * g ↑n

Tactic:
rw [mul_add, 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
⊢ ∑ i, C * (a i * T (r i n)) + C * g ↑n = ∑ i, a i * (C * T (r i n)) + C * g ↑n
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 : ℕ
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
z : ℕ
hz : z ∈ cf.eval (Nat.pair (unpair n).1 (i + ((unpair n).2 + 1)))
z0 : ¬z = 0
⊢ z ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2))

Tactic:
by simpa [add_comm, add_left_comm] using hz

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
⊢ ↑n ^ (p a b + 1) / ↑n ^ (p a b + 1) * (1 - c₃) * c₂ * g ↑n / c₁ ^ (p a b + 1) =
    (1 - c₃) * c₂ / c₁ ^ (p a b + 1) * g ↑n

Tactic:
rw [div_self (by positivity), one_mul]

Goal state after:
α : 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
⊢ (1 - c₃) * c₂ * g ↑n / c₁ ^ (p a b + 1) = (1 - c₃) * c₂ / c₁ ^ (p a b + 1) * 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
⊢ (1 - c₃) * c₂ / c₁ ^ (p a b + 1) * g ↑n ≥ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n

Tactic:
gcongr; exact min_le_right _ _

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 * (l * m) ≤ m

Tactic:
h,

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
⊢ l ^ n * m ≤ m
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
⊢ l = m * l + n

Tactic:
h,

Goal state after:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
⊢ m∗ * n = m * (m∗ * n) + n
Module: Mathlib.Computability.DFA

Goal state before:
pp: case inr
α : 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)
this :
  ∀ (n m : Fin (Fintype.card σ + 1)),
    n ≠ m →
      M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x) →
        ↑n ≤ ↑m →
          ∃ q a b c,
            x = a ++ b ++ c ∧
              a.length + b.length ≤ Fintype.card σ ∧
                b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
hle : ¬↑n ≤ ↑m
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t

Tactic:
exact this m n hneq.symm heq.symm (le_of_not_ge hle)

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : M.evalFrom s x = s
hy : y ∈ {x}∗
⊢ M.evalFrom s y = s

Tactic:
Language.mem_kstar

Goal state after:
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : M.evalFrom s x = s
hy : ∃ L, y = L.flatten ∧ ∀ y ∈ L, y ∈ {x}
⊢ M.evalFrom s y = s
Module: Mathlib.Computability.DFA

Goal state before:
pp: case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
⊢ a' ++ b' ++ c' ∈ M.accepts

Tactic:
have h := M.evalFrom_of_pow hb hb'

Goal state after:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
⊢ a' ++ b' ++ c' ∈ M.accepts
Module: Mathlib.Computability.DFA

Goal state before:
pp: case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
⊢ M.evalFrom (M.evalFrom (M.evalFrom M.start a') b') c' ∈ M.accept

Tactic:
h,

Goal state after:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
⊢ M.evalFrom (M.evalFrom M.start a') c' ∈ M.accept
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case pos
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : n = 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

pp: case neg
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
· 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]

Goal state after:
case neg
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
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
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
⊢ ∃ 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:
refine ⟨c₂^p, hc₂p, ?_⟩
      refine ⟨c₁^p, hc₁p, ?_⟩
      filter_upwards [eventually_gt_atTop 0, hfnew, hpos,
          (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hpos]
          with x _ hf₁ hf_pos hf_pos₂
      intro u hu
      refine ⟨?lb, ?ub⟩
      case lb => calc
        c₂ ^ p * (f x) ^ p = (c₂ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₂_mem) (le_of_lt hf_pos)]
          _ ≤ _ := rpow_le_rpow_of_nonpos (hf_pos₂ u hu.1) (hf₁ u hu).2 (le_of_lt hp)
      case ub => calc
        (f u) ^ p ≤ (c₁ * f x) ^ p := by
              exact rpow_le_rpow_of_nonpos (by positivity) (hf₁ u hu).1 (le_of_lt hp)
          _ = _ := by rw [← mul_rpow (le_of_lt hc₁_mem) (le_of_lt hf_pos)]

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
⊢ (a.testBit i ^^ v.testBit i) = false

Tactic:
h,

Goal state after:
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 ^^ v.testBit i) = false
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
⊢ (b.testBit i ^^ v.testBit i) = false

Tactic:
h,

Goal state after:
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 ^^ v.testBit i) = false
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
⊢ (c.testBit i ^^ v.testBit i) = false

Tactic:
h,

Goal state after:
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 ^^ v.testBit i) = false
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
h,

Goal state after:
case mp
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, l₁ ++ some a :: l₂ = replicate m none ++ some a :: replicate n none
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case h
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w✝ = replicate m none ++ some a :: replicate n none
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ (replicate n none).reduceOption = []

Tactic:
h,

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

Goal state before:
pp: case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
w✝¹ w✝ : List (Option α)
h : l = w✝¹ ++ some a :: w✝
hl₁ : w✝¹.reduceOption = l'
hl₂ : w✝.reduceOption = []
⊢ l.reduceOption = l' ++ [a]

Tactic:
h,

Goal state after:
case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
w✝¹ w✝ : List (Option α)
h : l = w✝¹ ++ some a :: w✝
hl₁ : w✝¹.reduceOption = l'
hl₂ : w✝.reduceOption = []
⊢ (w✝¹ ++ some a :: w✝).reduceOption = l' ++ [a]
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a ≤ b → b ≤ c → a ≤ c

Tactic:
intro a b c

Goal state after:
α : Type u_1
a b c : PosNum
⊢ a ≤ b → b ≤ c → a ≤ c
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left✝¹ : s₂ ∈ M.accept
s₁ : σ
left✝ : s₁ ∈ M.start
h : s₂ ∈ M.evalFrom {s₁} x
⊢ ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'

Tactic:
mem_evalFrom_iff_exists_path

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left✝¹ : s₂ ∈ M.accept
s₁ : σ
left✝ : s₁ ∈ M.start
h : ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
⊢ ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ castNum <$> (pos p).ppred = (↑(pos p)).ppred

Tactic:
rw [ppred, Option.map_eq_map, Option.map_some, Nat.ppred_eq_some.2]
    rw [PosNum.pred'_to_nat, Nat.succ_pred_eq_of_pos (PosNum.to_nat_pos _)]
    rfl

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun a ↦ ¬p a
⊢ ∀ (a : α),
    ∀ x ∈ Part.map (fun b ↦ true) (Part.assert (p a) fun x ↦ Part.some ()),
      ∀ y ∈ Part.map (fun b ↦ false) (Part.assert ((fun a ↦ ¬p a) a) fun x ↦ Part.some ()), x = y

Tactic:
intro a x hx y hy

Goal state after:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun a ↦ ¬p a
a : α
x : Bool
hx : x ∈ Part.map (fun b ↦ true) (Part.assert (p a) fun x ↦ Part.some ())
y : Bool
hy : y ∈ Part.map (fun b ↦ false) (Part.assert ((fun a ↦ ¬p a) a) fun x ↦ Part.some ())
⊢ x = y
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
L R : ListBlank Γ
⊢ move Dir.right (mk' L R) = mk' (ListBlank.cons R.head L) R.tail

Tactic:
by
  simp only [Tape.move, Tape.mk']

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
⊢ stepAux (write (enc a).toList q) v (trTape' enc0 L (ListBlank.cons b R)) =
    stepAux q v (trTape' enc0 (ListBlank.cons a L) R)

Tactic:
by
  simp only [trTape', ListBlank.cons_flatMap]
  suffices ∀ {L' R'} (l₁ l₂ l₂' : List Bool) (_ : l₂'.length = l₂.length),
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
      stepAux q v (Tape.mk' (L'.append (List.reverseAux l₂ l₁)) R') by
    exact this [] _ _ ((enc b).2.trans (enc a).2.symm)
  clear a b L R
  intro L' R' l₁ l₂ l₂' e
  induction l₂ generalizing l₁ l₂' with
  | nil => cases List.length_eq_zero_iff.1 e; rfl
  | cons a l₂ IH =>
    rcases l₂' with - | ⟨b, l₂'⟩ <;>
      simp only [List.length_nil, List.length_cons, Nat.succ_inj, reduceCtorEq] at e
    rw [List.reverseAux, ← IH (a :: l₁) l₂' e]
    simp [stepAux, ListBlank.append, write]

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

Goal state before:
pp: case pos.hn
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = tl.length
⊢ (List.map some tl).reverse.length ≤ i

Tactic:
h,

Goal state after:
case pos.hn
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = tl.length
⊢ (List.map some tl).reverse.length ≤ tl.length
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: c : Code
h : c.Ok
v : List ℕ
⊢ StateTransition.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v

Tactic:
h,

Goal state after:
c : Code
h : c.Ok
v : List ℕ
⊢ (do
      let v ← c.eval v
      StateTransition.eval step (Cfg.ret Cont.halt v)) =
    Cfg.halt <$> c.eval v
Module: Mathlib.Topology.Separation.Profinite

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

Tactic:
Subtype.image_preimage_coe

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

Goal state before:
pp: case mpr.inl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v'✝ : List ℕ
he✝¹ : v'✝ ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v'✝)
hr : x ∈ eval step (stepRet k v'✝)
v : List ℕ
he✝ : v'✝ ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
he : Sum.inl v'✝ ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
v' : List ℕ
he₁ : v' ∈ f.eval v
he₂ : (if v'.headI = 0 then Sum.inl v'.tail else Sum.inr v'.tail) = Sum.inl v'✝
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
split_ifs at he₂ with h

Goal state after:
case pos
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v'✝ : List ℕ
he✝¹ : v'✝ ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v'✝)
hr : x ∈ eval step (stepRet k v'✝)
v : List ℕ
he✝ : v'✝ ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
he : Sum.inl v'✝ ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Sum.inl v'.tail = Sum.inl v'✝
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)