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

Goal state before:
pp: case succ.prec.succ.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ : ℕ
⊢ (Option.none.bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    Option.none.bind fun i ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))

pp: case succ.prec.succ.some
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ val✝ : ℕ
⊢ ((some val✝).bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    (some val✝).bind fun i ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))

Tactic:
· rfl

Goal state after:
case succ.prec.succ.some
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ val✝ : ℕ
⊢ ((some val✝).bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    (some val✝).bind fun i ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case zero
⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero

pp: case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n

Tactic:
· rfl

Goal state after:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
a : α
⊢ l.reduceOption = [a] ↔ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
dsimp [reduceOption]
  constructor
  · intro h
    rw [filterMap_eq_cons_iff] at h
    obtain ⟨l₁, _, l₂, h, hl₁, ⟨⟩, hl₂⟩ := h
    rw [filterMap_eq_nil_iff] at hl₂
    apply eq_replicate_of_mem at hl₁
    apply eq_replicate_of_mem at hl₂
    rw [h, hl₁, hl₂]
    use l₁.length, l₂.length
  · intro ⟨_, _, h⟩
    simp only [h, filterMap_append, filterMap_cons_some, filterMap_replicate_of_none, id_eq,
      nil_append, Option.some.injEq]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ (∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}) → x ∈ M.accepts

pp: case mpr
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}

Tactic:
· rintro ⟨S, hS₁, hS₂⟩
    rwa [Set.mem_singleton_iff.mp hS₂] at hS₁

Goal state after:
case mpr
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
eval,

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

Goal state before:
pp: n : ℕ
f : ℕ →. ℕ
g : List.Vector ℕ n → ℕ
hf : Partrec' fun v ↦ f v.head
hg : Partrec' ↑g
⊢ Partrec' fun v ↦ f (g v)

Tactic:
by
  simpa using hf.comp' (Partrec'.cons hg Partrec'.nil)

Goal state after:
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₂ * ‖g u‖ ≤ c₂ * (c₄ * ‖g x‖)

Tactic:
by gcongr; exact (hg_bound u hu).2

Goal state after:
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:
rcases f (a ::ᵥ v) with - | c <;> intro this

Goal state after:
case refine_2.zero
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)
this : true = (ofNat (Option ℕ) 0).isSome
⊢ b = pred 0 ↔ ofNat (Option ℕ) 0 = some b

case refine_2.succ
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)
c : ℕ
this : true = (ofNat (Option ℕ) (c + 1)).isSome
⊢ b = (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l l₁ l₂ : List Γ
⊢ BlankExtends l₁ l → BlankExtends l₂ l → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

Tactic:
rintro ⟨i, rfl⟩ ⟨j, e⟩ h; use i - j
  refine List.append_cancel_right (e.symm.trans ?_)
  rw [List.append_assoc, ← List.replicate_add, Nat.sub_add_cancel]
  apply_fun List.length at e
  simp only [List.length_append, List.length_replicate] at e
  rwa [← Nat.add_le_add_iff_left, e, Nat.add_le_add_iff_right]

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

Goal state before:
pp: case cons
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝) (head (Quotient.mk'' (head✝ :: tail✝)) :: (head✝ :: tail✝).tail)

Tactic:
· rfl

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p : α → Prop
⊢ ComputablePred p ↔ REPred p ∧ REPred fun a ↦ ¬p a

Tactic:
by
  classical exact computable_iff_re_compl_re

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refl.none
σ₁ : 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
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
hfc : f₁ c₁ = none
⊢ none = none

pp: case refl.some
σ₁ : 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
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
d₁ : σ₁
hfc : f₁ c₁ = some d₁
⊢ some d₁ = none

Tactic:
· rfl

Goal state after:
case refl.some
σ₁ : 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
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
d₁ : σ₁
hfc : f₁ c₁ = some d₁
⊢ some d₁ = none
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ ((move Dir.right)^[0] T).head = T.nth ↑0

pp: case succ
Γ : Type u_1
inst✝ : Inhabited Γ
n✝ : ℕ
a✝ : ∀ (T : Tape Γ), ((move Dir.right)^[n✝] T).head = T.nth ↑n✝
T : Tape Γ
⊢ ((move Dir.right)^[n✝ + 1] T).head = T.nth ↑(n✝ + 1)

Tactic:
· rfl

Goal state after:
case succ
Γ : Type u_1
inst✝ : Inhabited Γ
n✝ : ℕ
a✝ : ∀ (T : Tape Γ), ((move Dir.right)^[n✝] T).head = T.nth ↑n✝
T : Tape Γ
⊢ ((move Dir.right)^[n✝ + 1] T).head = T.nth ↑(n✝ + 1)
Module: Mathlib.Computability.Reduce

Goal state before:
pp: case h.a
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
φ : Sort ?u.20
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p✝ : Set ℕ
⊢ ManyOneEquiv (toNat p✝) (toNat p✝)

Tactic:
· rfl

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

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

Tactic:
subst h

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 Λ
q₁ : Stmt Γ Λ σ
hs : True
h : q₁ = halt
⊢ SupportsStmt S q₁

Tactic:
subst h

Goal state after:
case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
hs : True
⊢ SupportsStmt S halt
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
h : q₁ = goto l
⊢ SupportsStmt S q₁

Tactic:
subst h

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

Goal state before:
pp: case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
hs : True
h : q₁ = halt
⊢ SupportsStmt S q₁

Tactic:
subst h

Goal state after:
case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
hs : True
⊢ SupportsStmt S halt
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
IH :
  ∀ (t : List α),
    t.length < x.length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ (∃ S, x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true) → P.star.rmatch x = true

Tactic:
rintro ⟨S, hsum, helem⟩

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
IH :
  ∀ (t : List α),
    t.length < x.length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
S : List (List α)
hsum : x = S.flatten
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
⊢ P.star.rmatch x = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mpr.nil
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
IH :
  ∀ (t : List α),
    t.length < [].length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
hsum : [] = S.flatten
⊢ P.star.rmatch [] = true

pp: case mpr.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
hsum : a :: x = S.flatten
⊢ P.star.rmatch (a :: x) = true

Tactic:
· rfl

Goal state after:
case mpr.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
hsum : a :: x = S.flatten
⊢ P.star.rmatch (a :: x) = true
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.one
⊢ true = (↑one).testBit 0

pp: case pos.zero.bit1
m : PosNum
⊢ true = (↑m.bit1).testBit 0

pp: case pos.zero.bit0
m : PosNum
⊢ false = (↑m.bit0).testBit 0

pp: case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ false = (↑one).testBit (n✝ + 1)

pp: case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit1).testBit (n✝ + 1)

pp: case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit0).testBit (n✝ + 1)

Tactic:
· rfl

Goal state after:
case pos.zero.bit1
m : PosNum
⊢ true = (↑m.bit1).testBit 0

case pos.zero.bit0
m : PosNum
⊢ false = (↑m.bit0).testBit 0

case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ false = (↑one).testBit (n✝ + 1)

case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit1).testBit (n✝ + 1)

case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit0).testBit (n✝ + 1)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' : List ℕ
h1 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: ↑v)
this :
  ∀ (v₁ : List ℕ),
    v' ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          v₁ →
      ∀ (n_1 : ℕ),
        v₁ = n_1 :: ↑v →
          (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = [v'.headI.pred]

Tactic:
by exact this _ h1 0 rfl (by rintro _ ⟨⟩)

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

Goal state before:
pp: case right.e_a.e_a.nil
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) → σ
e : S k = []
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[[].length] (Tape.mk' ∅ (addBottom L)))).head.2 k = [].head?

pp: case right.e_a.e_a.cons
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) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[(head✝ :: tail✝).length] (Tape.mk' ∅ (addBottom L)))).head.2 k =
    (head✝ :: tail✝).head?

Tactic:
· rfl

Goal state after:
case right.e_a.e_a.cons
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) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[(head✝ :: tail✝).length] (Tape.mk' ∅ (addBottom L)))).head.2 k =
    (head✝ :: tail✝).head?
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case pos
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
⊢ none = default

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:
· rfl

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 ≤ i
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: case fst
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
z : ↑Z.toTop
hfst : (ConcreteCategory.hom (a ≫ fst f g)) z = (ConcreteCategory.hom (b ≫ fst f g)) z
hsnd : (ConcreteCategory.hom (a ≫ snd f g)) z = (ConcreteCategory.hom (b ≫ snd f g)) z
⊢ (↑((ConcreteCategory.hom a) z)).1 = (↑((ConcreteCategory.hom b) z)).1

pp: case snd
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
z : ↑Z.toTop
hfst : (ConcreteCategory.hom (a ≫ fst f g)) z = (ConcreteCategory.hom (b ≫ fst f g)) z
hsnd : (ConcreteCategory.hom (a ≫ snd f g)) z = (ConcreteCategory.hom (b ≫ snd f g)) z
⊢ (↑((ConcreteCategory.hom a) z)).2 = (↑((ConcreteCategory.hom b) z)).2

Tactic:
· exact hfst

Goal state after:
case snd
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
z : ↑Z.toTop
hfst : (ConcreteCategory.hom (a ≫ fst f g)) z = (ConcreteCategory.hom (b ≫ fst f g)) z
hsnd : (ConcreteCategory.hom (a ≫ snd f g)) z = (ConcreteCategory.hom (b ≫ snd f g)) z
⊢ (↑((ConcreteCategory.hom a) z)).2 = (↑((ConcreteCategory.hom b) z)).2
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacksOfInclusions P
X : CompHausLike P
⊢ ∀ {Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)

Tactic:
Y

Goal state after:
P : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacksOfInclusions P
X Y : CompHausLike P
⊢ ∀ {Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X : CompHausLike P
⊢ ∀ {Y Z : CompHausLike P} (f : X ⟶ Y) (g : Z ⟶ Y) [EffectiveEpi g], ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f

Tactic:
Y

Goal state after:
P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X Y : CompHausLike P
⊢ ∀ {Z : CompHausLike P} (f : X ⟶ Y) (g : Z ⟶ Y) [EffectiveEpi g], ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f