internlm/Lean-Github huggingface dataset:
Theorem: FinDenumerable.decode_fin_inj
Proof state before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ w✝¹ = w✝ ↔ Encodable.encode w✝¹ = Encodable.encode w✝
Tactic:
apply Iff.symm
Proof state after:
case h
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ Encodable.encode w✝¹ = Encodable.encode w✝ ↔ w✝¹ = w✝
Theorem: FinDenumerable.decode_fin_inj
Proof state before:
case h
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ Encodable.encode w✝¹ = Encodable.encode w✝ ↔ w✝¹ = w✝
Tactic:
apply Encodable.encode_inj
Proof state after:
no goals
Theorem: FinDenumerable.encodek_fin_left_inverse
Proof state before:
α : Type u_1
inst✝ : FinDenumerable α
⊢ Function.LeftInverse decode_fin encode_fin
Tactic:
intro _
Proof state after:
α : Type u_1
inst✝ : FinDenumerable α
x✝ : α
⊢ decode_fin (encode_fin x✝) = x✝
Theorem: FinDenumerable.encodek_fin_left_inverse
Proof state before:
α : Type u_1
inst✝ : FinDenumerable α
x✝ : α
⊢ decode_fin (encode_fin x✝) = x✝
Tactic:
simp [encode_fin, decode_fin]
Proof state after:
no goals
Theorem: FinDenumerable.decodenk
Proof state before:
α : Type u_1
inst : FinDenumerable α
⊢ ∀ (n : Fin (Fintype.card α)), encode_fin (decode_fin n) = n
Tactic:
simp [encode_fin, Fin.ext_iff, decode_fin]
Proof state after:
α : Type u_1
inst : FinDenumerable α
⊢ ∀ (n : Fin (Fintype.card α)), Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Theorem: FinDenumerable.decodenk
Proof state before:
α : Type u_1
inst : FinDenumerable α
⊢ ∀ (n : Fin (Fintype.card α)), Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Tactic:
intro n
Proof state after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Theorem: FinDenumerable.decodenk
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Tactic:
have ⟨ a, ph ⟩ := fin_preimage_exists n
Proof state after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
ph : Encodable.encode a = ↑n
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Theorem: FinDenumerable.decodenk
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
ph : Encodable.encode a = ↑n
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Tactic:
simp [<- ph]
Proof state after:
no goals
Theorem: FinDenumerable.encode_fin_range
Proof state before:
α : Type u_1
inst : FinDenumerable α
⊢ ↑(Set.range encode_fin) ≃ Fin (Fintype.card α)
Tactic:
rw [Function.Surjective.range_eq _]
Proof state after:
α : Type u_1
inst : FinDenumerable α
⊢ ↑Set.univ ≃ Fin (Fintype.card α)

α : Type u_1
inst : FinDenumerable α
⊢ Function.Surjective encode_fin
Theorem: FinDenumerable.encode_fin_range
Proof state before:
α : Type u_1
inst : FinDenumerable α
⊢ ↑Set.univ ≃ Fin (Fintype.card α)

α : Type u_1
inst : FinDenumerable α
⊢ Function.Surjective encode_fin
Tactic:
exact Equiv.Set.univ (Fin (Fintype.card α))
Proof state after:
α : Type u_1
inst : FinDenumerable α
⊢ Function.Surjective encode_fin
Theorem: FinDenumerable.encode_fin_range
Proof state before:
α : Type u_1
inst : FinDenumerable α
⊢ Function.Surjective encode_fin
Tactic:
exact encode_fin_bijective.surjective
Proof state after:
no goals
Theorem: FinDenumerable.equiv_fin
Proof state before:
α : Type u_1
inst : FinDenumerable α
⊢ α ≃ Fin (Fintype.card α)
Tactic:
have tmp := Equiv.ofLeftInverse encode_fin (fun _ => inst.decode_fin) (fun _ => encodek_fin_left_inverse)
Proof state after:
α : Type u_1
inst : FinDenumerable α
tmp : α ≃ ↑(Set.range encode_fin)
⊢ α ≃ Fin (Fintype.card α)
Theorem: FinDenumerable.equiv_fin
Proof state before:
α : Type u_1
inst : FinDenumerable α
tmp : α ≃ ↑(Set.range encode_fin)
⊢ α ≃ Fin (Fintype.card α)
Tactic:
apply Equiv.trans tmp encode_fin_range
Proof state after:
no goals
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r : Run (fromNFA M) a✝¹ a✝
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h : NFA.Run.last r ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted r h') ∈ (fromNFA M).F
Tactic:
cases r
Proof state after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : NFA.Run.last (NFA.Run.final a✝¹ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F

case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step a✝² x✝ r✝ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.step a✝² x✝ r✝ h✝) h') ∈ (fromNFA M).F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : NFA.Run.last (NFA.Run.final a✝¹ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F

case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step a✝² x✝ r✝ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.step a✝² x✝ r✝ h✝) h') ∈ (fromNFA M).F
Tactic:
. dsimp [NFA.Run.last, fromNFA] at h
  rw [Finset.mem_filter] at h
  dsimp [RunFromRestricted, NFA.Run.last, fromNFA]
  apply Eq.subst (propext $ Finset.mem_filter.symm) (motive := id); simp
  constructor
  rw [Finset.attach_eq_univ]; dsimp [Finset.univ]
  apply Fintype.complete
  have ⟨_, q, _, _⟩ := h
  exists q; constructor; constructor
  apply Finset.mem_of_subset
  repeat { assumption }
Proof state after:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step a✝² x✝ r✝ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.step a✝² x✝ r✝ h✝) h') ∈ (fromNFA M).F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step a✝² x✝ r✝ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.step a✝² x✝ r✝ h✝) h') ∈ (fromNFA M).F
Tactic:
. dsimp [RunFromRestricted, NFA.Run.last]
  apply RunFromRestricted_final
  dsimp [NFA.Run.last] at h
  assumption
Proof state after:
no goals
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : NFA.Run.last (NFA.Run.final a✝¹ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F
Tactic:
dsimp [NFA.Run.last, fromNFA] at h
Proof state after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F
Tactic:
rw [Finset.mem_filter] at h
Proof state after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F
Tactic:
dsimp [RunFromRestricted, NFA.Run.last, fromNFA]
Proof state after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ self✝ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ self✝ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
Tactic:
apply Eq.subst (propext $ Finset.mem_filter.symm) (motive := id)
Proof state after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ id (self✝ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑self✝, q ∈ M.F)
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ id (self✝ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑self✝, q ∈ M.F)
Tactic:
simp
Proof state after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ self✝ ∈ Finset.attach Finset.univ ∧
    ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ self✝ ∈ Finset.attach Finset.univ ∧
    ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
constructor
Proof state after:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ self✝ ∈ Finset.attach Finset.univ

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ self✝ ∈ Finset.attach Finset.univ

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
rw [Finset.attach_eq_univ]
Proof state after:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ self✝ ∈ Finset.univ

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ self✝ ∈ Finset.univ

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
dsimp [Finset.univ]
Proof state after:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ self✝ ∈ Finset.attach Fintype.elems

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ self✝ ∈ Finset.attach Fintype.elems

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
apply Fintype.complete
Proof state after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
have ⟨_, q, _, _⟩ := h
Proof state after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
exists q
Proof state after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ∃ (b : ↑q ∈ M.Q), { val := ↑q, property := b } ∈ ↑self✝ ∧ { val := ↑q, property := b } ∈ M.F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ∃ (b : ↑q ∈ M.Q), { val := ↑q, property := b } ∈ ↑self✝ ∧ { val := ↑q, property := b } ∈ M.F
Tactic:
constructor
Proof state after:
case final.right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ?final.right.w } ∈ ↑self✝ ∧ { val := ↑q, property := ?final.right.w } ∈ M.F

case final.right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ↑q ∈ M.Q