mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
;

Goal state after:
case zero.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
⊢ ↑0 = 0
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‖)
⊢ c₂ * (c₄ * |g x|) = c₂ * c₄ * |g x|

Tactic:
;

Goal state after:
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‖)
⊢ c₂ * (c₄ * |g x|) = c₂ * c₄ * |g x|
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
⊢ true = (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome → (b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b)

Tactic:
;

Goal state after:
case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
⊢ true = (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome → (b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b)
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' fun v ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
g : ℕ → Part ℕ := fun n₁ ↦ (↑(decode n₁)).bind fun a ↦ Part.map encode (f a)
i : List.Vector ℕ n
⊢ ((↑(decode (encode i))).bind fun a ↦ Part.map encode (f a)) = f i

Tactic:
;

Goal state after:
this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' fun v ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
g : ℕ → Part ℕ := fun n₁ ↦ (↑(decode n₁)).bind fun a ↦ Part.map encode (f a)
i : List.Vector ℕ n
⊢ ((↑(decode (encode i))).bind fun a ↦ Part.map encode (f a)) = f i
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
x✝ : ℝ
⊢ f x✝ = (g + (f - g)) x✝

Tactic:
;

Goal state after:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
x✝ : ℝ
⊢ f x✝ = (g + (f - g)) x✝
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length
⊢ BlankExtends (l ++ List.replicate i default) (l ++ List.replicate j default)

Tactic:
;

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length
⊢ BlankExtends (l ++ List.replicate i default) (l ++ List.replicate j default)
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refl
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ hab : b ∈ f a
hbc : ReflTransGen (fun a b ↦ b ∈ f a) b c
⊢ Reaches f b c

Tactic:
;

Goal state after:
case refl
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ hab : b ∈ f a
hbc : ReflTransGen (fun a b ↦ b ∈ f a) b c
⊢ Reaches f b c
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ BlankExtends l₁ l₂

Tactic:
;

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ BlankExtends l₁ l₂
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type ?u.5
f : σ → Option σ
b : σ
C : σ → Sort u_1
a : σ
h : b ∈ eval f a
H : (a : σ) → b ∈ eval f a → ((a' : σ) → f a = some a' → C a') → C a
a' : σ
ha' : b ∈ PFun.fix (fun s ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
h' : (a'' : σ) → Sum.inr a'' ∈ Part.some ((f a').elim (Sum.inl a') Sum.inr) → C a''
b' : σ
e : f a' = some b'
⊢ Sum.inr b' = (some b').elim (Sum.inl a') Sum.inr

Tactic:
;

Goal state after:
σ : Type ?u.5
f : σ → Option σ
b : σ
C : σ → Sort u_1
a : σ
h : b ∈ eval f a
H : (a : σ) → b ∈ eval f a → ((a' : σ) → f a = some a' → C a') → C a
a' : σ
ha' : b ∈ PFun.fix (fun s ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
h' : (a'' : σ) → Sum.inr a'' ∈ Part.some ((f a').elim (Sum.inl a') Sum.inr) → C a''
b' : σ
e : f a' = some b'
⊢ Sum.inr b' = (some b').elim (Sum.inl a') Sum.inr
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : 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
e : f a = none
⊢ Sum.inl ?m.69 = none.elim (Sum.inl a) Sum.inr

Tactic:
;

Goal state after:
σ : 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
e : f a = none
⊢ Sum.inl ?m.69 = none.elim (Sum.inl a) Sum.inr
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.6
inst✝ : Inhabited Γ
a : Γ
l : ListBlank Γ
a✝ : List Γ
i : ℕ
⊢ mk (a :: a✝) = mk (a :: (a✝ ++ List.replicate i default))

Tactic:
exact Quotient.sound' (Or.inl ⟨i, rfl⟩)

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : α → Bool
h : Computable f
⊢ ComputablePred fun a ↦ f a = true

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
h : Computable f
⊢ ComputablePred fun a ↦ f a = true
Module: Mathlib.Computability.RE

Goal state before:
pp: case unit
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a ↦ f a = true
n : α
⊢ (PUnit.unit ∈ bif f n then Part.some () else Part.none) ↔ PUnit.unit ∈ Part.assert (f n = true) fun x ↦ Part.some ()

Tactic:
;

Goal state after:
case unit
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a ↦ f a = true
n : α
⊢ (PUnit.unit ∈ bif f n then Part.some () else Part.none) ↔ PUnit.unit ∈ Part.assert (f n = true) fun x ↦ Part.some ()
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab✝¹ : b₁ ∈ eval f₁ a₁
ab✝ : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
this :
  match f₁ b₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
⊢ f₂ b₂ = none

Tactic:
;

Goal state after:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab✝¹ : b₁ ∈ eval f₁ a₁
ab✝ : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
this :
  match f₁ b₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
⊢ f₂ b₂ = none
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ : Type u_1
σ₂ : Type u_2
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₂ b₂ : σ₂
h : f₂ a₂ = f₂ b₂
⊢ (match none with
    | some b₁ => Reaches₁ f₂ a₂ (tr b₁)
    | none => f₂ a₂ = none) ↔
    match none with
    | some b₁ => Reaches₁ f₂ b₂ (tr b₁)
    | none => f₂ b₂ = none

Tactic:
;

Goal state after:
σ₁ : Type u_1
σ₂ : Type u_2
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₂ b₂ : σ₂
h : f₂ a₂ = f₂ b₂
⊢ (match none with
    | some b₁ => Reaches₁ f₂ a₂ (tr b₁)
    | none => f₂ a₂ = none) ↔
    match none with
    | some b₁ => Reaches₁ f₂ b₂ (tr b₁)
    | none => f₂ b₂ = none
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
c : Option σ
h₁ : EvalsTo f a (some b)
h₂ : EvalsTo f b c
⊢ (flip bind f)^[h₂.steps + h₁.steps] (some a) = c

Tactic:
Function.iterate_add_apply,

Goal state after:
σ : Type u_1
f : σ → Option σ
a b : σ
c : Option σ
h₁ : EvalsTo f a (some b)
h₂ : EvalsTo f b c
⊢ (flip bind f)^[h₂.steps] ((flip bind f)^[h₁.steps] (some a)) = c
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.9
Γ' : Type ?u.8
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
l : List Γ
i : ℕ
⊢ mk (List.map f.f l) = mk (List.map f.f (l ++ List.replicate i default))

Tactic:
;

Goal state after:
Γ : Type ?u.9
Γ' : Type ?u.8
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
l : List Γ
i : ℕ
⊢ mk (List.map f.f l) = mk (List.map f.f (l ++ List.replicate i default))
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (proj i).f (L.nth n) = L.nth n i

Tactic:
;

Goal state after:
ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (proj i).f (L.nth n) = L.nth n i
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
i : ℕ
⊢ mk (List.flatMap f l) = mk (List.flatMap f (l ++ List.replicate i default))

Tactic:
;

Goal state after:
Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
i : ℕ
⊢ mk (List.flatMap f l) = mk (List.flatMap f (l ++ List.replicate i default))
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ mk (List.flatMap f l) = mk (List.flatMap f (l ++ List.replicate i default))

Tactic:
;

Goal state after:
Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ mk (List.flatMap f l) = mk (List.flatMap f (l ++ List.replicate i default))
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ List.flatMap f l ++ List.flatMap f (List.replicate i default) = List.flatMap f l ++ List.replicate (n * i) default

Tactic:
;

Goal state after:
Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ List.flatMap f l ++ List.flatMap f (List.replicate i default) = List.flatMap f l ++ List.replicate (n * i) default
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
| T.nth (i + 1)

Tactic:
;

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
| T.nth (i + 1)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ write { head := head✝, left := left✝, right := right✝ }.head { head := head✝, left := left✝, right := right✝ } =
    { head := head✝, left := left✝, right := right✝ }

Tactic:
;

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ write { head := head✝, left := left✝, right := right✝ }.head { head := head✝, left := left✝, right := right✝ } =
    { head := head✝, left := left✝, right := right✝ }
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ (map f { head := head✝, left := left✝, right := right✝ }).head =
    f.f { head := head✝, left := left✝, right := right✝ }.head

Tactic:
;

Goal state after:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ (map f { head := head✝, left := left✝, right := right✝ }).head =
    f.f { head := head✝, left := left✝, right := right✝ }.head
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
b head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (write b { head := head✝, left := left✝, right := right✝ }) =
    write (f.f b) (map f { head := head✝, left := left✝, right := right✝ })

Tactic:
;

Goal state after:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
b head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (write b { head := head✝, left := left✝, right := right✝ }) =
    write (f.f b) (map f { head := head✝, left := left✝, right := right✝ })
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ RecursiveIn O g

Tactic:
;

Goal state after:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ RecursiveIn O g
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ Nat.RecursiveIn O g

Tactic:
;

Goal state after:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ Nat.RecursiveIn O g
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
s : Part ℕ
hf : RecursiveIn {fun x ↦ s} f
g : ℕ →. ℕ
hg : g ∈ {fun x ↦ s}
⊢ Partrec fun x ↦ s

Tactic:
;

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
s : Part ℕ
hf : RecursiveIn {fun x ↦ s} f
g : ℕ →. ℕ
hg : g ∈ {fun x ↦ s}
⊢ Partrec fun x ↦ s
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
⊢ p a

Tactic:
;

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
⊢ p 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
⊢ p a

Tactic:
;

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
⊢ p a
Module: Mathlib.Computability.Reduce

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
⊢ q = (q ∘ ⇑e) ∘ ⇑e.symm

Tactic:
;

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
⊢ q = (q ∘ ⇑e) ∘ ⇑e.symm
Module: Mathlib.Computability.Reduce

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
x✝ : β
⊢ q x✝ = ((q ∘ ⇑e) ∘ ⇑e.symm) x✝

Tactic:
;

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
x✝ : β
⊢ q x✝ = ((q ∘ ⇑e) ∘ ⇑e.symm) x✝
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
l : Γ → σ → Λ
h₁₂ : q₁ = goto l
⊢ q₀ ∈ {goto l}

Tactic:
subst h₁₂

Goal state after:
case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
l : Γ → σ → Λ
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ q₀ ∈ {goto l}
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
l : Γ → σ → Λ
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ q₀ ∈ {goto l}

Tactic:
;

Goal state after:
case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
l : Γ → σ → Λ
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ q₀ ∈ {goto l}
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}

Tactic:
subst h₁₂

Goal state after:
case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ halt
⊢ q₀ ∈ {halt}
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ halt
⊢ q₀ ∈ {halt}

Tactic:
;

Goal state after:
case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ halt
⊢ q₀ ∈ {halt}
Module: Mathlib.Computability.Reduce

Goal state before:
pp: case h
p✝ : Set ℕ
⊢ of p✝ ≤ of p✝

Tactic:
;

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

Goal state before:
pp: case h
p✝ : Set ℕ
⊢ p✝ ≤₀ p✝

Tactic:
;

Goal state after:
case h
p✝ : Set ℕ
⊢ p✝ ≤₀ p✝
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
d₁ d₂ : ManyOneDegree
a b c d : ℕ → Prop
hl₁ : a ≤₀ b
hr₁ : b ≤₀ a
hl₂ : c ≤₀ d
hr₂ : d ≤₀ c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [of_eq_of]

Goal state after:
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
d₁ d₂ : ManyOneDegree
a b c d : ℕ → Prop
hl₁ : a ≤₀ b
hr₁ : b ≤₀ a
hl₂ : c ≤₀ d
hr₂ : d ≤₀ c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S (branch p q₁ q₂)
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S (branch p q₁ q₂)
⊢ SupportsStmt S (branch p q₁ q₂)

pp: case branch.inr.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₁
⊢ SupportsStmt S q₁✝

pp: case branch.inr.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S q₁✝

Tactic:
;

Goal state after:
case branch.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S (branch p q₁ q₂)
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S (branch p q₁ q₂)
⊢ SupportsStmt S (branch p q₁ q₂)

case branch.inr.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₁
⊢ SupportsStmt S q₁✝

case branch.inr.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S q₁✝
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
l : Γ → σ → Λ
hs : ∀ (a : Γ) (v : σ), l a v ∈ S
⊢ SupportsStmt S (goto l)

Tactic:
;

Goal state after:
case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
l : Γ → σ → Λ
hs : ∀ (a : Γ) (v : σ), l a v ∈ S
⊢ SupportsStmt S (goto l)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
hs : True
⊢ SupportsStmt S halt

Tactic:
;

Goal state after:
case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
hs : True
⊢ SupportsStmt S halt