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

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) ↔ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
constructor

Goal state after:
case mp
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) → x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

case mpr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T → ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] ↔ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] → ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ (∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []) → l.reduceOption = l' ++ [a]
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true

Tactic:
by
  rw [reduceOption_length_eq, List.length_filter_eq_length_iff]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : εNFA α σ
⊢ M.evalFrom ∅ [] = ∅

Tactic:
evalFrom_nil,

Goal state after:
case nil
α : Type u
σ : Type v
M : εNFA α σ
⊢ M.εClosure ∅ = ∅
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Tactic:
constructor

Goal state after:
case mp
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept → ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

case mpr
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ (∃ S ∈ M.accept, S ∈ M.evalFrom M.start x) → M.toDFA.eval x ∈ M.toDFA.accept
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
start : σ
s : List α
⊢ List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}

Tactic:
induction s generalizing start with
  | nil => tauto
  | cons a s ih =>
    rw [List.foldl, List.foldl,
      show M.toNFA.stepSet {start} a = {M.step start a} by simp [NFA.stepSet]]
    tauto

Goal state after:
Module: Mathlib.Computability.NFA

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

Tactic:
constructor

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

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.NFA

Goal state before:
pp: α : Type u
L : Language α
h : L.IsRegular
σ : Type
w✝ : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ M.toNFA.reverse.toDFA.accepts = L.reverse

Tactic:
ext

Goal state after:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
w✝ : Fintype σ
M : DFA α σ
hM : M.accepts = L
x✝ : List α
⊢ x✝ ∈ M.toNFA.reverse.toDFA.accepts ↔ x✝ ∈ L.reverse
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ s₂ ∈ M.evalFrom {s₁} [] ↔ ∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'

Tactic:
evalFrom_nil,

Goal state after:
case nil
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ s₂ ∈ M.εClosure {s₁} ↔ ∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : 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:
constructor

Goal state after:
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'

case nil.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x') → ∃ n, M.IsPath s₁ s₂ (List.replicate n none)
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton
α : 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₂ : σ
⊢ (∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) ↔ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
constructor

Goal state after:
case append_singleton.mp
α : 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₂ : σ
⊢ (∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) → ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

case append_singleton.mpr
α : 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', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x') → ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ ↑n.size + 1 = (↑n.bit0).size

Tactic:
size_to_nat n,

Goal state after:
n : PosNum
⊢ (↑n).size + 1 = (↑n.bit0).size
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ ↑n.size + 1 = (↑n.bit1).size

Tactic:
size_to_nat n,

Goal state after:
n : PosNum
⊢ (↑n).size + 1 = (↑n.bit1).size
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
ppred,

Goal state after:
p : PosNum
⊢ castNum <$> some p.pred' = (↑(pos p)).ppred
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:
gcongr; exact (hg_bound u hu).2

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

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

Tactic:
ext

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

Goal state before:
pp: f₁ f₂ : ℕ → ℕ
hf₁ : Computable f₁
hf₂ : Computable f₂
c : ℕ → Prop
inst✝ : DecidablePred c
hc : ComputablePred c
⊢ Computable fun k ↦ if c k then f₁ k else f₂ k

Tactic:
by
  simpa [Bool.cond_decide] using hc.decide.cond hf₁ hf₂

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
l : List Γ
⊢ append (l₁ ++ l₂) (mk l) = append l₁ (append l₂ (mk l))

Tactic:
simp only [ListBlank.append_mk, List.append_assoc]

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ Supports M Set.univ

Tactic:
constructor

Goal state after:
case left
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ default ∈ Set.univ

case right
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ ∀ {q : Λ} {a : Γ} {q' : Λ} {s : Stmt Γ}, (q', s) ∈ M q a → q ∈ Set.univ → q' ∈ Set.univ
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ Tape Γ

Tactic:
constructor

Goal state after:
case head
Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ Γ

case left
Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ ListBlank Γ

case right
Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ ListBlank Γ
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case zero
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' fun x ↦ 0

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case succ
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' ↑Nat.succ

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case left
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' fun n ↦ ↑(Option.some (unpair n).1)

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case right
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' fun n ↦ ↑(Option.some (unpair n).2)

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case zero
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
⊢ Nat.Partrec fun x ↦ 0

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case succ
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
⊢ Nat.Partrec ↑Nat.succ

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case left
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
⊢ Nat.Partrec fun n ↦ ↑(Option.some (unpair n).1)

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case right
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
⊢ Nat.Partrec fun n ↦ ↑(Option.some (unpair n).2)

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case zero
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ Nat.RecursiveIn O (pure 0)

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case succ
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ Nat.RecursiveIn O ↑Nat.succ

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case left
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ Nat.RecursiveIn O ↑fun n ↦ (unpair n).1

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case right
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ Nat.RecursiveIn O ↑fun n ↦ (unpair n).2

Tactic:
constructor

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail✝ = true ↔ P.rmatch tail✝ = true ∨ Q.rmatch tail✝ = true
P Q : RegularExpression α
⊢ (P.deriv head✝ + Q.deriv head✝).rmatch tail✝ = true ↔
    P.rmatch (head✝ :: tail✝) = true ∨ Q.rmatch (head✝ :: tail✝) = true

Tactic:
exact ih _ _

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
x : List α
⊢ (P + Q).rmatch x = true ↔ P.rmatch x = true ∨ Q.rmatch x = true

Tactic:
by
  induction x generalizing P Q with
  | nil => simp only [rmatch, matchEpsilon, Bool.or_eq_true_iff]
  | cons _ _ ih =>
    rw [rmatch, deriv_add]
    exact ih _ _

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (P.matchEpsilon && Q.matchEpsilon) = true ↔ ∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
constructor

Goal state after:
case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (P.matchEpsilon && Q.matchEpsilon) = true → ∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

case nil.mpr
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) → (P.matchEpsilon && Q.matchEpsilon) = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true ↔
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
constructor

Goal state after:
case pos.mp
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true →
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

case pos.mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
⊢ (∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) →
    (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true
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✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ TM0.Supports (tr M) ↑(trStmts M S)

Tactic:
constructor

Goal state after:
case left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default ∈ ↑(trStmts M S)

case right
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ ∀ {q : Λ' M} {a : Γ} {q' : Λ' M} {s : TM0.Stmt Γ}, (q', s) ∈ tr M q a → q ∈ ↑(trStmts M S) → q' ∈ ↑(trStmts M S)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.1 ∈ TM1.stmts M S ∧ default.2 ∈ Finset.univ

Tactic:
constructor

Goal state after:
case left.left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.1 ∈ TM1.stmts M S

case left.right
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.2 ∈ Finset.univ
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ↔
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
constructor

Goal state after:
case neg.mp
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) →
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

case neg.mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) →
    ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux (i + 1) f)

Tactic:
constructor

Goal state after:
case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun v ↦ f (true ::ᵥ v)))

case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun v ↦ f (false ::ᵥ v)))
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : 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)
⊢ P.star.rmatch x = true ↔ ∃ S, x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
constructor

Goal state after:
case mp
α : 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)
⊢ P.star.rmatch x = true → ∃ S, x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

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
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
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)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ a :: x = ((a :: t) :: S').flatten ∧ ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true

Tactic:
constructor

Goal state after:
case h.left
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
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)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ a :: x = ((a :: t) :: S').flatten

case h.right
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
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)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : ℕ
⊢ ↑0 = ↑zero <<< n

Tactic:
symm
    apply Nat.zero_shiftLeft

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

Goal state before:
pp: case write.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ q' ∈ writes q → q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
q' : Λ' Γ Λ σ
hq : q' ∈ writes q
⊢ SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
exact IH.2 _ hq

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

Goal state before:
pp: case rfind
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)]
x : List ℕ
⊢ (∃
      a ∈
        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),
      x = [a.headI.pred]) ↔
    ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x

Tactic:
constructor

Goal state after:
case rfind.mp
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)]
x : List ℕ
⊢ (∃
      a ∈
        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),
      x = [a.headI.pred]) →
    ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x

case rfind.mpr
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)]
x : List ℕ
⊢ (∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x) →
    ∃
      a ∈
        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),
      x = [a.headI.pred]