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

Goal state before:
pp: case refine_2.prec
cf cg : Code
pf : Nat.Partrec cf.eval
pg : Nat.Partrec cg.eval
⊢ Nat.Partrec (cf.prec cg).eval

Tactic:
exact pf.prec pg

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
⊢ b * x ≤ x

Tactic:
nth_rewrite 2 [← one_mul x]

Goal state after:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
⊢ b * x ≤ 1 * x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
⊢ b * x ≤ x

Tactic:
nth_rewrite 2 [← one_mul x]

Goal state after:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
⊢ b * x ≤ 1 * x
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
⊢ 1 + l∗ * l = l∗

Tactic:
by
  rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hpr
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
⊢ Primrec fun a ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
    let y ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    some (Nat.pair x y)

Tactic:
have cg := (Primrec.fst.comp Primrec.snd).comp
      (Primrec.snd (α := (List (List (Option ℕ)) × ℕ) × ℕ)
        (β := Code × Code × Option ℕ × Option ℕ))

Goal state after:
case hpr
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
⊢ Primrec fun a ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
    let y ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    some (Nat.pair x y)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hco
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
⊢ Primrec fun a ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) x

Tactic:
have cg := (Primrec.fst.comp Primrec.snd).comp
      (Primrec.snd (α := (List (List (Option ℕ)) × ℕ) × ℕ)
        (β := Code × Code × Option ℕ × Option ℕ))

Goal state after:
case hco
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
⊢ Primrec fun a ↦ do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) x
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hpc
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    Nat.casesOn (unpair a.1.1.2).2 (lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) z) fun y ↦ do
      let i ← lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z y)
      lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) (Nat.pair z (Nat.pair y i))

Tactic:
have cg := (Primrec.fst.comp Primrec.snd).comp
      (Primrec.snd (α := (List (List (Option ℕ)) × ℕ) × ℕ)
        (β := Code × Code × Option ℕ × Option ℕ))

Goal state after:
case hpc
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    Nat.casesOn (unpair a.1.1.2).2 (lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) z) fun y ↦ do
      let i ← lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z y)
      lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) (Nat.pair z (Nat.pair y i))
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inl
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 ^^^ v < a

pp: case inr.inl
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 ^^^ v < b

pp: case inr.inr
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 ^^^ v < c

Tactic:
all_goals
    refine lt_of_testBit i ?_ h fun j hj => ?_
    · rw [testBit_xor, h, hi]
      rfl
    · simp only [testBit_xor, hi' _ hj, Bool.bne_false]

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

Goal state before:
pp: case neg
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
· simp only [mod_two_ne_zero] at h
    simp only [h, xor_mod_two_eq_one]
    lia

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: α : Type u_1
Γ : Type u_2
e : Encoding α Γ
⊢ Function.Injective e.encode

Tactic:
refine fun _ _ h => Option.some_injective _ ?_

Goal state after:
α : Type u_1
Γ : Type u_2
e : Encoding α Γ
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ some x✝¹ = some x✝
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s : σ
hs : s ∈ M.εClosure ∅
⊢ False

Tactic:
induction hs

Goal state after:
case base
α : Type u
σ : Type v
M : εNFA α σ
s s✝ : σ
a✝ : s✝ ∈ ∅
⊢ False

case step
α : Type u
σ : Type v
M : εNFA α σ
s s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure ∅ s✝
a_ih✝ : False
⊢ False
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ∀ (a b c : Num), a + b + c = a + (b + c)

Tactic:
transfer

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil.mp
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ n, M.IsPath s₁ s₂ (List.replicate n none)) → ∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'

Tactic:
intro ⟨n, _⟩

Goal state after:
case nil.mp
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h✝ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ ∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ∀ (a : Num), a ≤ a

Tactic:
transfer

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

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

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a + b = b + a

Tactic:
transfer

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

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

Tactic:
transfer

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 ∧ s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
rw [mem_εClosure_iff_exists, 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.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), 1 * a = a

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), a * 1 = a

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a * b = b * a

Tactic:
transfer

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a * (b + c) = a * b + a * c

Tactic:
transfer

Goal state after:
α : Type u_1
a✝ b✝ c✝ : PosNum
⊢ ↑a✝ * (↑b✝ + ↑c✝) = ↑a✝ * ↑b✝ + ↑a✝ * ↑c✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), (a + b) * c = a * c + b * c

Tactic:
transfer

Goal state after:
α : Type u_1
a✝ b✝ c✝ : PosNum
⊢ ↑c✝ * (↑a✝ + ↑b✝) = ↑a✝ * ↑c✝ + ↑b✝ * ↑c✝
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
transfer

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

Goal state before:
pp: a : PosNum
⊢ a.sub' 1 = a.pred'.toZNum

Tactic:
cases a <;> rfl

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

Goal state before:
pp: a : PosNum
⊢ sub' 1 a = a.pred'.toZNumNeg

Tactic:
cases a <;> rfl

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_1.e_a
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = ↑(some (ofNat (Option ℕ) (f (n ::ᵥ v))).isSome)

Tactic:
cases f (n ::ᵥ v)

Goal state after:
case refine_1.e_a.zero
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ 0)) = ↑(some (ofNat (Option ℕ) 0).isSome)

case refine_1.e_a.succ
n✝¹ : ℕ
f : List.Vector ℕ (n✝¹ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝¹
b a n n✝ : ℕ
⊢ Part.some (decide (1 ≤ n✝ + 1)) = ↑(some (ofNat (Option ℕ) (n✝ + 1)).isSome)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case h
Γ : 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
⊢ l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default

Tactic:
List.append_assoc,

Goal state after:
case h
Γ : 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
⊢ l₁ ++ List.replicate i default = l₁ ++ (List.replicate (i - j) default ++ List.replicate j default)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
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' (le_of_not_ge hl)

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1.some
σ : 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'
⊢ Reaches f a b ∧ f b = none

Tactic:
rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩)

Goal state after:
case refine_1.some.inl
σ : 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.inl b ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)
⊢ Reaches f a b ∧ f b = none

case refine_1.some.inr
σ : 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'
w✝ : σ
h : Sum.inr w✝ ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) w✝
⊢ Reaches f a b ∧ f b = none
Module: Mathlib.Computability.TuringMachine.Tape

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

Tactic:
refine Quotient.sound' (Or.inl ?_)

Goal state after:
Γ : Type ?u.5
inst✝ : Inhabited Γ
l : ListBlank Γ
a : List Γ
i : ℕ
⊢ BlankExtends a.tail (a ++ List.replicate i default).tail
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : ComputablePred p
⊢ Computable fun a ↦ decide (p a)

Tactic:
by
  convert! hp.choose_spec

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

Goal state before:
pp: case branch.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch p q₁ q₂)
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
unfold stmts₁ at h₀₁
      exact h₀₁

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ of p = of q ↔ ManyOneEquiv p q

Tactic:
of,

Goal state after:
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ Quotient.mk'' (toNat p) = of q ↔ ManyOneEquiv p q
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ Quotient.mk'' (toNat p) = of q ↔ ManyOneEquiv p q

Tactic:
of,

Goal state after:
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ Quotient.mk'' (toNat p) = Quotient.mk'' (toNat q) ↔ ManyOneEquiv p q
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ some q₂ ∈ stmts M S → some q₁ ∈ stmts M S

Tactic:
by
  simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]
  exact fun l ls h₂ ↦ ⟨_, ls, stmts₁_trans h₂ h₁⟩

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
c' : Cfg Γ Λ σ
h₁ : c' ∈ step M { l := some l₁, var := v, Tape := T }
h₂ : { l := some l₁, var := v, Tape := T }.l ∈ Finset.insertNone S
⊢ c'.l ∈ Finset.insertNone S

Tactic:
replace h₂ := ss.2 _ (Finset.some_mem_insertNone.1 h₂)
    simp only [step, Option.mem_def, Option.some.injEq] at h₁; subst c'
    revert h₂; induction M l₁ generalizing v T with intro hs
    | branch p q₁' q₂' IH₁ IH₂ =>
      unfold stepAux; cases p T.1 v
      · exact IH₂ _ _ hs.2
      · exact IH₁ _ _ hs.1
    | goto => exact Finset.some_mem_insertNone.2 (hs _ _)
    | halt => apply Multiset.mem_cons_self
    | _ _ q IH => exact IH _ _ hs

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

Goal state before:
pp: case branch.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch f q₁ q₂)
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
unfold stmts₁ at h₀₁
      exact h₀₁

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

Goal state before:
pp: case load.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
a✝ : σ → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (load a✝ q)
IH : load a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)

Tactic:
unfold stmts₁ at h₀₁
      exact h₀₁

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

Goal state before:
pp: case push.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k✝ : K
a✝ : σ → Γ k✝
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (push k✝ a✝ q)
IH : push k✝ a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (push k✝ a✝ q) (stmts₁ q)

Tactic:
unfold stmts₁ at h₀₁
      exact h₀₁

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

Goal state before:
pp: case peek.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (peek k✝ a✝ q)
IH : peek k✝ a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (peek k✝ a✝ q) (stmts₁ q)

Tactic:
unfold stmts₁ at h₀₁
      exact h₀₁

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

Goal state before:
pp: case pop.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (pop k✝ a✝ q)
IH : pop k✝ a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

Tactic:
unfold stmts₁ at h₀₁
      exact h₀₁

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
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ some q₂ ∈ stmts M S → some q₁ ∈ stmts M S

Tactic:
by
  simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]
  exact fun l ls h₂ ↦ ⟨_, ls, stmts₁_trans h₂ h₁⟩

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
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ (bif a then
      stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))) =
    stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

Tactic:
cases a <;> rfl

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

Goal state before:
pp: m : Num
n : ℕ
⊢ ↑(m >>> n) = ↑m >>> n

Tactic:
by
  obtain - | m := m <;> dsimp only [← shiftr_eq_shiftRight, shiftr]
  · symm
    apply Nat.zero_shiftRight
  induction n generalizing m with
  | zero => cases m <;> rfl
  | succ n IH => ?_
  have hdiv2 : ∀ m, Nat.div2 (m + m) = m := by intro; rw [Nat.div2_val]; lia
  obtain - | m | m := m <;> dsimp only [PosNum.shiftr, ← PosNum.shiftr_eq_shiftRight]
  · rw [Nat.shiftRight_eq_div_pow]
    symm
    apply Nat.div_eq_of_lt
    simp
  · trans
    · apply IH
    change Nat.shiftRight m n = Nat.shiftRight (m + m + 1) (n + 1)
    rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]
    apply congr_arg fun x => Nat.shiftRight x n
    simp [-add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, hdiv2]
  · trans
    · apply IH
    change Nat.shiftRight m n = Nat.shiftRight (m + m) (n + 1)
    rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]
    apply congr_arg fun x => Nat.shiftRight x n
    simp [-add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, hdiv2]

Goal state after: