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

Goal state before:
pp: x✝ : Unit
p : ℕ
⊢ G
      (x✝,
          List.map
            (fun n ↦
              let a := ofNat (ℕ × Code) n;
              List.map (evaln a.1 a.2) (List.range a.1))
            (List.range p)).2 =
    some
      (let a := ofNat (ℕ × Code) p;
      List.map (evaln a.1 a.2) (List.range a.1))

Tactic:
by

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

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ 2 ∣ 4

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: this :
  Primrec₂ fun x n ↦
    let a := ofNat (ℕ × Code) n;
    List.map (evaln a.1 a.2) (List.range a.1)
x✝ : (ℕ × Code) × ℕ
k : ℕ
c : Code
n : ℕ
⊢ ((let a := ofNat (ℕ × Code) (encode ((k, c), n).1);
          List.map (evaln a.1 a.2) (List.range a.1))[((k, c), n).2]?.bind
      fun b ↦ (((k, c), n), b).2) =
    evaln ((k, c), n).1.1 ((k, c), n).1.2 ((k, c), n).2

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c : Code
n x : ℕ
⊢ x ∈ c.eval n ↔ x ∈ rfindOpt fun k ↦ evaln k c n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: a : Code × ℕ
⊢ (rfindOpt fun b ↦
      evaln (((a, b).2, (a, b).1.1), (a, b).1.2).1.1 (((a, b).2, (a, b).1.1), (a, b).1.2).1.2
        (((a, b).2, (a, b).1.1), (a, b).1.2).2) =
    a.1.eval a.2

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y ↦ do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this : Partrec₂ g
cg : Code
eg : cg.eval = fun n ↦ (↑(decode n)).bind fun a ↦ Part.map encode ((fun p ↦ g p.1 p.2) a)
⊢ ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y ↦ do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this✝ : Partrec₂ g
cg : Code
eg : cg.eval = fun n ↦ (↑(decode n)).bind fun a ↦ Part.map encode ((fun p ↦ g p.1 p.2) a)
eg' : ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)
F : ℕ → Code := fun x ↦ f (cg.curry x)
this : Computable F
cF : Code
eF : cF.eval = fun n ↦ (↑(decode n)).bind fun a ↦ Part.map encode (↑F a)
⊢ cF.eval (encode cF) = Part.some (encode (F (encode cF)))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : Code → ℕ →. ℕ
hf : Partrec₂ f
cf : Code
ef : cf.eval = fun n ↦ (↑(decode n)).bind fun a ↦ Part.map encode ((fun p ↦ f p.1 p.2) a)
c : Code
e : (cf.curry (encode c)).eval = c.eval
n : ℕ
⊢ c.eval n = f c n

Tactic:
by

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

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ 2 ∣ 4

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ Countable { f // Partrec f }

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝¹ x✝ : { f // Computable f }
h : (fun f ↦ ⟨↑↑f, ⋯⟩) x✝¹ = (fun f ↦ ⟨↑↑f, ⋯⟩) x✝
⊢ ↑↑x✝¹ = ↑↑x✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑↑p.bit0 = ↑p.bit0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑↑p.bit1 = ↑p.bit1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : PosNum
⊢ ↑↑n = ↑n

Tactic:
by

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

Goal state before:
pp: n : PosNum
⊢ 1 + n = n.succ

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Encoding

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: b : Bool
⊢ sectionΓ'Bool (inclusionBoolΓ' b) = b

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: n : PosNum
⊢ decodePosNum (encodePosNum n) = n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: n : Num
⊢ decodeNum (encodeNum n) = n

Tactic:
by

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

Goal state before:
pp: n : PosNum
⊢ n + 1 = n.succ

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: n : ℕ
⊢ decodeNat (encodeNat n) = n

Tactic:
by

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

Goal state before:
pp: b : PosNum
⊢ ↑(1 + b) = ↑1 + ↑b

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: x : ℕ
⊢ decodeNat (List.map sectionΓ'Bool (List.map inclusionBoolΓ' (encodeNat x))) = x

Tactic:
by

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

Goal state before:
pp: a : PosNum
⊢ ↑(a + 1) = ↑a + ↑1

Tactic:
by

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

Goal state before:
pp: x n m : ℕ
h : x < 2 ^ n
⊢ x <<< m < 2 ^ (n + m)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: α : Type u_1
β : Type u_2
Γ₁ : Type u_3
Γ₂ : Type u_4
ea : Encoding α Γ₁
eb : Encoding β Γ₂
x : α × β
⊢ Option.map₂ Prod.mk
      (ea.decode (List.filterMap Sum.getLeft? (List.map Sum.inl (ea.encode x.1) ++ List.map Sum.inr (eb.encode x.2))))
      (eb.decode
        (List.filterMap Sum.getRight? (List.map Sum.inl (ea.encode x.1) ++ List.map Sum.inr (eb.encode x.2)))) =
    some x

Tactic:
by

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

Goal state before:
pp: b : PosNum
⊢ 1 + b.succ = (1 + b).succ

Tactic:
by

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

Goal state before:
pp: x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n ||| x < 2 ^ (n + m)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
a : α
⊢ M.stepSet ∅ a = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s : σ
a : α
⊢ M.stepSet {s} a = M.step s a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
a : α
⊢ M.stepSet (S ∪ T) a = M.stepSet S a ∪ M.stepSet T a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x y : List α
⊢ M.evalFrom S (x ++ y) = M.evalFrom (M.evalFrom S x) y

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
κ : ι → Sort u_2
f : (i : ι) → κ i → Set σ
x : List α
⊢ M.evalFrom (⋃ i, ⋃ j, f i j) x = ⋃ i, ⋃ j, M.evalFrom (f i j) x

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
⊢ M.evalFrom S x = ⋃ s ∈ S, M.evalFrom {s} x

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
x : List α
⊢ s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ [] ∈ M.acceptsFrom S ↔ ∃ s ∈ S, s ∈ M.accept

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
x : List α
⊢ a :: x ∈ M.acceptsFrom S ↔ x ∈ M.acceptsFrom (M.stepSet S a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
x : α
l : List (Option α)
⊢ (some x :: l).reduceOption = x :: l.reduceOption

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ (none :: l).reduceOption = l.reduceOption

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List (Option α)
f : α → β
⊢ (map (Option.map f) l).reduceOption = map f l.reduceOption

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ (replicate n none).reduceOption = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
⊢ (fun x ↦ a :: x) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.stepSet S a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x y : List α
⊢ x ++ y ∈ M.acceptsFrom S ↔ y ∈ M.acceptsFrom (M.evalFrom S x)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
⊢ (fun x_1 ↦ x ++ x_1) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.evalFrom S x)

Tactic:
by

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
⊢ b * x ≤ 1 * x

Tactic:
by

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

Goal state after:
Module: Mathlib.Data.List.ReduceOption

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
⊢ M.acceptsFrom (S ∪ T) = M.acceptsFrom S + M.acceptsFrom T

Tactic:
by

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

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit0.cmp b.bit0) (↑a.bit0 < ↑b.bit0) (a.bit0 = b.bit0) (↑b.bit0 < ↑a.bit0)

Tactic:
by

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
⊢ 1 * x = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length = (filter Option.isSome l).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.length = l.reduceOption.length + (filter Option.isNone l).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length ≤ l.length

Tactic:
by

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

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
⊢ M.acceptsFrom (⋃ i, s i) = ⋃ i, M.acceptsFrom (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
κ : ι → Sort u_2
f : (i : ι) → κ i → Set σ
⊢ M.acceptsFrom (⋃ i, ⋃ j, f i j) = ⋃ i, ⋃ j, M.acceptsFrom (f i j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length < l.length ↔ none ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
x : Option α
⊢ [x].reduceOption = x.toList

Tactic:
by

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

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit0.cmp b.bit1) (↑a.bit0 < ↑b.bit1) (a.bit0 = b.bit1) (↑b.bit1 < ↑a.bit0)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : Option α
⊢ (l.concat x).reduceOption = l.reduceOption ++ x.toList

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : α
⊢ (l.concat (some x)).reduceOption = l.reduceOption.concat x

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
⊢ M.stepSet {s | s ∈ S ∧ p} a = {s | s ∈ M.stepSet S a ∧ p}

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : α
⊢ x ∈ l.reduceOption ↔ some x ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : α
⊢ (∃ i, l[i]? = some (some x)) ↔ ∃ i, l.reduceOption[i]? = some x

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
p : Prop
x : List α
⊢ x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
a : α
⊢ M.eval (x ++ [a]) = M.stepSet (M.eval x) a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s t : σ
x : List α
h : t ∈ M.evalFrom {s} []
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
h : s ∈ M.εClosure S
⊢ ∃ t ∈ S, s ∈ M.εClosure {t}

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
⊢ (∃ t ∈ S, s ∈ M.εClosure {t}) → s ∈ M.εClosure S

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
a : α
⊢ M.stepSet ∅ a = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
⊢ M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s t : σ
x✝ : List α
a : α
x : List α
h : t ∈ M.evalFrom {s} (a :: x)
⊢ ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s✝ t : σ
x : List α
p : Nonempty (M.Path s✝ t x)
s : σ
⊢ s ∈ M.evalFrom {s} []

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s✝ t✝ : σ
x✝ : List α
p : Nonempty (M.Path s✝ t✝ x✝)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
⊢ t ∈ M.evalFrom {s} (a :: x)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.accepts ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, Nonempty (M.Path s t x)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
x : List α
⊢ M.evalFrom ∅ x = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
⊢ M.toDFA.accepts = M.accepts

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ M.accepts
hlen : Fintype.card (Set σ) ≤ x.length
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Tactic:
by

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

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit1.cmp b.bit0) (↑a.bit1 < ↑b.bit0) (a.bit1 = b.bit0) (↑b.bit0 < ↑a.bit1)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s : σ
S : Set σ
x : List α
⊢ s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ M.IsPath s t [] ↔ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
⊢ M.IsPath s t [a] → t ∈ M.step s a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
⊢ M.toNFA.accepts = M.accepts

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
⊢ M.reverse.reverse = M

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
⊢ t ∈ M.step s a → M.IsPath s t [a]

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
⊢ Disjoint S (M.reverse.stepSet S' a) ↔ Disjoint S' (M.stepSet S a)

Tactic:
by

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

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit1.cmp b.bit1) (↑a.bit1 < ↑b.bit1) (a.bit1 = b.bit1) (↑b.bit1 < ↑a.bit1)

Tactic:
by

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

Goal state before:
pp: m n : PosNum
h : Ordering.casesOn Ordering.lt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
by

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

Goal state before:
pp: m n : PosNum
h : Ordering.casesOn Ordering.eq (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
by

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

Goal state before:
pp: m n : PosNum
h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.gt = Ordering.lt

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
⊢ M.IsPath s u (x ++ y) → ∃ t, M.IsPath s t x ∧ M.IsPath t u y

Tactic:
by

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

Goal state before:
pp: m n : PosNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
by

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

Goal state before:
pp: n : Num
⊢ n + 0 = n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
S S' : Set σ
h : Disjoint S (M.reverse.evalFrom S' x)
⊢ Disjoint S' (M.evalFrom S x.reverse)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.reverse.accepts ↔ x.reverse ∈ M.accepts

Tactic:
by

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

Goal state before:
pp: n : Num
⊢ 0 + n = n

Tactic:
by

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

Goal state before:
pp: p : PosNum
⊢ pos p + 1 = (pos p).succ

Tactic:
by

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

Goal state before:
pp: n : Num
⊢ 0 + n.succ = (0 + n).succ

Tactic:
by

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

Goal state before:
pp: ⊢ ofNat' 0 = 0

Tactic:
by

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

Goal state before:
pp: ⊢ ofNat' 1 = 1

Tactic:
by

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

Goal state before:
pp: ⊢ ofNat' (0 + 1) = ofNat' 0 + 1

Tactic:
by

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

Goal state after: