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
⊢ (1 + ε ↑n) * asympBound g a b n ≤ C * T n

Tactic:
have g_pos : 0 ≤ g n := R.g_nonneg n (by positivity)

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 * T 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
⊢ ↑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]; ring

Goal state after:
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 ^ 1 * m ^ n✝ * n ≤ m * l + n

Tactic:
pow_one,

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 * m ^ n✝ * n ≤ m * l + n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
H : ∀ᶠ (x : ℝ) in atTop, 0 < f x
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Tactic:
filter_upwards [H] with _ hx; exact (ne_of_lt hx).symm

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

Goal state before:
pp: f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
⊢ c₂⁻¹ > 0

Tactic:
by change 0 < c₂⁻¹; positivity

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 u ≤ 1 * log x

Tactic:
rw [one_mul]
    gcongr
    · calc 0 < b * x := by positivity
         _ ≤ u := by exact hu.1
    · exact hu.2

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

Goal state before:
pp: m n : ℕ
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
by_cases h : (m + n) % 2 = 0

Goal state after:
case pos
m n : ℕ
h : (m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

case neg
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2
Module: Mathlib.Computability.NFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
a : α
x : List α
ih : ∀ (s : ι → Set σ), M.evalFrom (⋃ i, s i) x = ⋃ i, M.evalFrom (s i) x
s : ι → Set σ
⊢ M.evalFrom (⋃ i, s i) (a :: x) = ⋃ i, M.evalFrom (s i) (a :: x)

Tactic:
simp [stepSet, Set.iUnion_comm (ι := σ) (ι' := ι), ih]

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

Goal state before:
pp: case one.one
⊢ Ordering.eq.swap = Ordering.eq

Tactic:
try { rfl }

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

Goal state before:
pp: case one.bit1
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

Tactic:
try { rfl }

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

Goal state before:
pp: case one.bit0
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

Tactic:
try { rfl }

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

Goal state before:
pp: case bit1.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

Tactic:
try { rfl }

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

Goal state before:
pp: case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

Tactic:
try { rfl }

Goal state after:
case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.lt Ordering.gt

Tactic:
try { rfl }

Goal state after:
case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.lt Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

Tactic:
try { rfl }

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

Goal state before:
pp: case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.gt Ordering.gt

Tactic:
try { rfl }

Goal state after:
case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.gt Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

Tactic:
try { rfl }

Goal state after:
case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝ : Num
⊢ x✝ * 0 = 0

Tactic:
by rw [← to_nat_inj, mul_to_nat, cast_zero, mul_zero]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
x : List α
⊢ (∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x') → x ∈ M.accepts

Tactic:
intro ⟨s₁, s₂, x', hs₁, hs₂, h⟩

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₁ s₂ : σ
x' : List (Option α)
hs₁ : s₁ ∈ M.start
hs₂ : s₂ ∈ M.accept
h : x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
⊢ x ∈ M.accepts
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero.zero
⊢ (zero.cmp zero).swap = zero.cmp zero

Tactic:
try { rfl }

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

Goal state before:
pp: case zero.pos
a✝ : PosNum
⊢ (zero.cmp (pos a✝)).swap = (pos a✝).cmp zero

Tactic:
try { rfl }

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

Goal state before:
pp: case pos.zero
a✝ : PosNum
⊢ ((pos a✝).cmp zero).swap = zero.cmp (pos a✝)

Tactic:
try { rfl }

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

Goal state before:
pp: case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)

Tactic:
try { rfl }

Goal state after:
case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound✝ : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ f u ≤ c₂ * ‖g u‖

Tactic:
rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1

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

Goal state before:
pp: case refine_1
Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : l₁.length ≤ l₂.length
h' : BlankExtends l₂ l₁
⊢ BlankExtends l₁ l₂

pp: case refine_2
Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : ¬l₁.length ≤ l₂.length
h' : BlankExtends l₁ l₂
⊢ BlankExtends l₂ l₁

Tactic:
· exact (BlankExtends.refl _).above_of_le h' hl

Goal state after:
case refine_2
Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : ¬l₁.length ≤ l₂.length
h' : BlankExtends l₁ l₂
⊢ BlankExtends l₂ l₁
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1.some.inr.refl
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
⊢ Reaches f a b ∧ f b = none

Tactic:
obtain ⟨h₁, h₂⟩ := IH a' e

Goal state after:
case refine_1.some.inr.refl
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
h₁ : Reaches f a' b
h₂ : f b = none
⊢ Reaches f a b ∧ f b = none
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1.some.inr.refl
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
h₁ : Reaches f a' b
h₂ : f b = none
⊢ Reaches f a b ∧ f b = none

Tactic:
exact ⟨ReflTransGen.head e h₁, h₂⟩

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α →. β
h : Partrec f
n : α
x✝ : Unit
⊢ x✝ ∈ Part.map (fun b ↦ ()) (f n) ↔ x✝ ∈ Part.assert ((fun a ↦ (f a).Dom) n) fun x ↦ Part.some ()

Tactic:
simp [Part.dom_iff_mem]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
a : Γ
⊢ map f (cons a l) = cons (f.f a) (map f l)

Tactic:
by
  refine (ListBlank.cons_head_tail _).symm.trans ?_
  simp only [ListBlank.head_map, ListBlank.head_cons, ListBlank.tail_map, ListBlank.tail_cons]

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
L R : ListBlank Γ
n : ℕ
⊢ (mk' L R).nth ↑n = R.nth n

Tactic:
rw [← Tape.right₀_nth, Tape.mk'_right₀]

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ r (g (f a))

Tactic:
← h₂,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ q (f a)
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ r (g (f a))

Tactic:
← h₂,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ q (f a)
Module: Mathlib.Computability.Reduce

Goal state before:
pp: d : ManyOneDegree
⊢ d ≤ d

Tactic:
induction d using ManyOneDegree.ind_on

Goal state after:
case h
p✝ : Set ℕ
⊢ of p✝ ≤ of p✝
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = false
⊢ TM0.step (tr M) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T } =
    TM0.step (tr M) { q := (some a✝, v), Tape := T }

Tactic:
simp only [TM0.step, tr, trAux, e]; rfl

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = true
⊢ TM0.step (tr M) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T } =
    TM0.step (tr M) { q := (some a✝¹, v), Tape := T }

Tactic:
simp only [TM0.step, tr, trAux, e]; rfl

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ L.nth n k = S.reverse[n]?

Tactic:
rw [← proj_map_nth, hL, ← List.map_reverse, ListBlank.nth_mk,
    List.getI_eq_getElem?_getD, List.getElem?_map]
  cases S.reverse[n]? <;> rfl

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f))
      (update S k
        (match StAct.peek f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => (S k).tail))

Tactic:
rw [Function.update_eq_self]

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) S
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
⊢ P.rmatch x = true ↔ x ∈ P.matches'

Tactic:
by
  induction P generalizing x with
  | zero =>
    rw [zero_def, zero_rmatch]
    tauto
  | epsilon =>
    rw [one_def, one_rmatch_iff, matches'_epsilon, Language.mem_one]
  | char =>
    rw [char_rmatch_iff]
    rfl
  | plus _ _ ih₁ ih₂ =>
    rw [plus_def, add_rmatch_iff, ih₁, ih₂]
    rfl
  | comp P Q ih₁ ih₂ =>
    simp only [comp_def, mul_rmatch_iff, matches'_mul, Language.mem_mul, *]
    tauto
  | star _ ih =>
    simp only [star_rmatch_iff, matches'_star, ih, Language.mem_kstar_iff_exists_nonempty, and_comm]

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

Goal state before:
pp: case peek
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) → σ
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (S k) k_1)).reverse) ∧
      TM1.stepAux q
          (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
          (Tape.move Dir.right (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L')))

Tactic:
rw [Function.update_eq_self]

Goal state after:
case peek
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) → σ
⊢ ∃ L',
    (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
      TM1.stepAux q
          (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
          (Tape.move Dir.right (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L')))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update S rev [] = S

Tactic:
← h₂,

Goal state after:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update S rev (S rev) = S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update S rev [] = S

Tactic:
← h₂,

Goal state after:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update S rev (S rev) = S
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
⊢ ∀ C ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c

Tactic:
intro C C_sub C_chain

Goal state after:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
⊢ ∃ s ∈ S, ∀ c ∈ C, s ⊆ c