internlm/Lean-Github huggingface dataset:
Theorem: totalDFA_del_star_eq
Proof state before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q' : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'
⊢ DFA.del_star_curried M xs q' =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
let q' : M.toTotalDFA.Q := ⟨ some q', Fintype.complete _ ⟩
Proof state after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'✝
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Theorem: totalDFA_del_star_eq
Proof state before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'✝
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
have : q'.val = some _ := rfl
Proof state after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'✝
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Theorem: totalDFA_del_star_eq
Proof state before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'✝
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
rw [<-this] at hd
Proof state after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Theorem: totalDFA_del_star_eq
Proof state before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
rw [Subtype.eq hd]
Proof state after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (q', xs))
Theorem: totalDFA_del_star_eq
Proof state before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (q', xs))
Tactic:
apply ih
Proof state after:
no goals
Theorem: Subtype.eq_iff
Proof state before:
α qs : Type
M : DFA α qs
p : α → Prop
x y : Subtype p
h : x = y
⊢ ↑x = ↑y
Tactic:
rw [h]
Proof state after:
no goals
Theorem: totalDFA_lang_eq
Proof state before:
α qs : Type
M : DFA α qs
⊢ DFA.AcceptedLanguage M = DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
apply Set.ext
Proof state after:
case h
α qs : Type
M : DFA α qs
⊢ ∀ (x : Word { x // x ∈ M.Z }), x ∈ DFA.AcceptedLanguage M ↔ x ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Theorem: totalDFA_lang_eq
Proof state before:
case h
α qs : Type
M : DFA α qs
⊢ ∀ (x : Word { x // x ∈ M.Z }), x ∈ DFA.AcceptedLanguage M ↔ x ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
intro w
Proof state after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ DFA.AcceptedLanguage M ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Theorem: totalDFA_lang_eq
Proof state before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ DFA.AcceptedLanguage M ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
rw [DFA.in_language_iff_del_star_final]
Proof state after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Theorem: totalDFA_lang_eq
Proof state before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
let w': Word M.toTotalDFA.Z := w
Proof state after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Theorem: totalDFA_lang_eq
Proof state before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
have w_cast : w = w' := rfl
Proof state after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Theorem: totalDFA_lang_eq
Proof state before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
rw [w_cast, TotalDFA.in_language_iff_del_star_final]
Proof state after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    TotalDFA.del_star' (DFA.toTotalDFA M) ((DFA.toTotalDFA M).q₀, w') ∈ (DFA.toTotalDFA M).F
Theorem: totalDFA_lang_eq
Proof state before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    TotalDFA.del_star' (DFA.toTotalDFA M) ((DFA.toTotalDFA M).q₀, w') ∈ (DFA.toTotalDFA M).F
Tactic:
conv =>
  right; congr;
  right; simp [DFA.toTotalDFA]; rfl
  simp [DFA.toTotalDFA]
Proof state after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some M.q₀, property := ⋯ }, w') ∈
      Finset.map { toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } M.F
Theorem: totalDFA_lang_eq
Proof state before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some M.q₀, property := ⋯ }, w') ∈
      Finset.map { toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } M.F
Tactic:
rw [Finset.mem_map]
Proof state after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    ∃ a ∈ M.F,
      { toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } a =
        TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some M.q₀, property := ⋯ }, w')
Theorem: totalDFA_lang_eq
Proof state before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    ∃ a ∈ M.F,
      { toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } a =
        TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some M.q₀, property := ⋯ }, w')
Tactic:
conv =>
  right; congr; intro;
  simp [Subtype.eq_iff, <-totalDFA_del_star_eq];
  rw [And.comm];
Proof state after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    ∃ x, ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Theorem: totalDFA_lang_eq
Proof state before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    ∃ x, ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Tactic:
constructor <;> intro ⟨x, l, r⟩ <;> exists x
Proof state after:
case h.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : x ∈ DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w') ∧ x ∈ M.F

case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Theorem: totalDFA_lang_eq
Proof state before:
case h.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : x ∈ DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w') ∧ x ∈ M.F

case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Tactic:
. simp [r, Option.mem_iff.mp l]; rfl
Proof state after:
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Theorem: totalDFA_lang_eq
Proof state before:
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Tactic:
. simp [l, r]; exact l.symm
Proof state after:
no goals
Theorem: totalDFA_lang_eq
Proof state before:
case h.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : x ∈ DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Tactic:
simp [r, Option.mem_iff.mp l]
Proof state after:
case h.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : x ∈ DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = some x
Theorem: totalDFA_lang_eq
Proof state before:
case h.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : x ∈ DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = some x
Tactic:
rfl
Proof state after:
no goals
Theorem: totalDFA_lang_eq
Proof state before:
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Tactic:
simp [l, r]
Proof state after:
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ DFA.del_star M (M.q₀, w') = some x
Theorem: totalDFA_lang_eq
Proof state before:
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ DFA.del_star M (M.q₀, w') = some x
Tactic:
exact l.symm
Proof state after:
no goals
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
α : Type u_1
L : Language α
u v : Word α
⊢ u ≃( L ) v ↔ ∀ (x : Word α), u * x ≃( L ) v * x
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
L : Language α
u v : Word α
⊢ u ≃( L ) v → ∀ (x : Word α), u * x ≃( L ) v * x

case mpr
α : Type u_1
L : Language α
u v : Word α
⊢ (∀ (x : Word α), u * x ≃( L ) v * x) → u ≃( L ) v
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mp
α : Type u_1
L : Language α
u v : Word α
⊢ u ≃( L ) v → ∀ (x : Word α), u * x ≃( L ) v * x

case mpr
α : Type u_1
L : Language α
u v : Word α
⊢ (∀ (x : Word α), u * x ≃( L ) v * x) → u ≃( L ) v
Tactic:
. intro h w x
  have := h (w * x)
  rw [<- Word.monoid.mul_assoc] at this
  rw [<- Word.monoid.mul_assoc] at this
  assumption
Proof state after:
case mpr
α : Type u_1
L : Language α
u v : Word α
⊢ (∀ (x : Word α), u * x ≃( L ) v * x) → u ≃( L ) v
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mpr
α : Type u_1
L : Language α
u v : Word α
⊢ (∀ (x : Word α), u * x ≃( L ) v * x) → u ≃( L ) v
Tactic:
. intro h w
  have := (h w) ε
  simp at this
  assumption
Proof state after:
no goals
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mp
α : Type u_1
L : Language α
u v : Word α
⊢ u ≃( L ) v → ∀ (x : Word α), u * x ≃( L ) v * x
Tactic:
intro h w x
Proof state after:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
Tactic:
have := h (w * x)
Proof state after:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * (w * x) ∈ L ↔ v * (w * x) ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * (w * x) ∈ L ↔ v * (w * x) ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
Tactic:
rw [<- Word.monoid.mul_assoc] at this
Proof state after:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * w * x ∈ L ↔ v * (w * x) ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * w * x ∈ L ↔ v * (w * x) ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
Tactic:
rw [<- Word.monoid.mul_assoc] at this
Proof state after:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * w * x ∈ L ↔ v * w * x ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * w * x ∈ L ↔ v * w * x ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
Tactic:
assumption
Proof state after:
no goals
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mpr
α : Type u_1
L : Language α
u v : Word α
⊢ (∀ (x : Word α), u * x ≃( L ) v * x) → u ≃( L ) v
Tactic:
intro h w
Proof state after:
case mpr
α : Type u_1
L : Language α
u v : Word α
h : ∀ (x : Word α), u * x ≃( L ) v * x
w : Word α
⊢ u * w ∈ L ↔ v * w ∈ L
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mpr
α : Type u_1
L : Language α
u v : Word α
h : ∀ (x : Word α), u * x ≃( L ) v * x
w : Word α
⊢ u * w ∈ L ↔ v * w ∈ L
Tactic:
have := (h w) ε
Proof state after:
case mpr
α : Type u_1
L : Language α
u v : Word α
h : ∀ (x : Word α), u * x ≃( L ) v * x
w : Word α
this : u * w * ε ∈ L ↔ v * w * ε ∈ L
⊢ u * w ∈ L ↔ v * w ∈ L
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mpr
α : Type u_1
L : Language α
u v : Word α
h : ∀ (x : Word α), u * x ≃( L ) v * x
w : Word α
this : u * w * ε ∈ L ↔ v * w * ε ∈ L
⊢ u * w ∈ L ↔ v * w ∈ L
Tactic:
simp at this
Proof state after:
case mpr
α : Type u_1
L : Language α
u v : Word α
h : ∀ (x : Word α), u * x ≃( L ) v * x
w : Word α
this : u * w ∈ L ↔ v * w ∈ L
⊢ u * w ∈ L ↔ v * w ∈ L
Theorem: MyhillNerodeRelation.right_congruence
Proof state before:
case mpr
α : Type u_1
L : Language α
u v : Word α
h : ∀ (x : Word α), u * x ≃( L ) v * x
w : Word α
this : u * w ∈ L ↔ v * w ∈ L
⊢ u * w ∈ L ↔ v * w ∈ L
Tactic:
assumption
Proof state after:
no goals
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
⊢ (∃ w, Language.isSingleton ({u * w, v * w} ∩ L)) → ¬u ≃( L ) v
Tactic:
intro ⟨ w, singl, singl_inter, h ⟩
Proof state after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
⊢ ¬u ≃( L ) v
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
⊢ ¬u ≃( L ) v
Tactic:
intro contra
Proof state after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
⊢ False
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
⊢ False
Tactic:
have h2 := contra w
Proof state after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
⊢ False
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
⊢ False
Tactic:
cases singl_inter.left
Proof state after:
case inl
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
h✝ : singl = u * w
⊢ False

case inr
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
h✝ : singl ∈ {v * w}
⊢ False
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
⊢ False
Tactic:
case inl e =>
  have vw_in_l := h2.mp $ e ▸ singl_inter.right
  have vw_eq_uw := e ▸ h (v*w) ⟨ Or.inr rfl, vw_in_l ⟩
  exact pre <| Eq.symm <| Word.mul_right_cancel vw_eq_uw
Proof state after:
no goals
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
⊢ False
Tactic:
case inr e =>
  have uw_in_l := h2.mpr $ e ▸ singl_inter.right
  have uw_eq_vw := e ▸ h (u*w) ⟨ Or.inl rfl, uw_in_l ⟩
  exact pre <| Word.mul_right_cancel uw_eq_vw
Proof state after:
no goals
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
⊢ False
Tactic:
have vw_in_l := h2.mp $ e ▸ singl_inter.right
Proof state after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
vw_in_l : v * w ∈ L
⊢ False
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
vw_in_l : v * w ∈ L
⊢ False
Tactic:
have vw_eq_uw := e ▸ h (v*w) ⟨ Or.inr rfl, vw_in_l ⟩
Proof state after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
vw_in_l : v * w ∈ L
vw_eq_uw : v * w = u * w
⊢ False