internlm/Lean-Github huggingface dataset:
Theorem: equiv_language_of_closure
Proof state before:
case h.mp
α : Type
R : RegExp α
cs : List α
⊢ (∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs) →
    cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
intro a1
Proof state after:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Theorem: equiv_language_of_closure
Proof state before:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
apply Exists.elim a1
Proof state after:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
⊢ ∀ (a : List (List α)),
    (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ a.join = cs →
      cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Theorem: equiv_language_of_closure
Proof state before:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
⊢ ∀ (a : List (List α)),
    (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ a.join = cs →
      cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
intro xs a2
Proof state after:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
xs : List (List α)
a2 : (∀ r ∈ xs, r ∈ RegExp.languageOf α R) ∧ xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Theorem: equiv_language_of_closure
Proof state before:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
xs : List (List α)
a2 : (∀ r ∈ xs, r ∈ RegExp.languageOf α R) ∧ xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
clear a1
Proof state after:
case h.mp
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2 : (∀ r ∈ xs, r ∈ RegExp.languageOf α R) ∧ xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Theorem: equiv_language_of_closure
Proof state before:
case h.mp
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2 : (∀ r ∈ xs, r ∈ RegExp.languageOf α R) ∧ xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
cases a2
Proof state after:
case h.mp.intro
α : Type
R : RegExp α
cs : List α
xs : List (List α)
left✝ : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
right✝ : xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
case _ a2_left a2_right =>
  simp only [← a2_right]
  cases xs
  case nil =>
    left
    simp
  case cons hd tl =>
    right
    simp at a2_left
    cases a2_left
    case _ a2_left_left a2_left_right =>
      apply Exists.intro hd
      tauto
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
simp only [← a2_right]
Proof state after:
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ xs.join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = xs.join
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ xs.join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = xs.join
Tactic:
cases xs
Proof state after:
case nil
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = [].join

case cons
α : Type
R : RegExp α
cs head✝ : List α
tail✝ : List (List α)
a2_left : ∀ r ∈ head✝ :: tail✝, r ∈ RegExp.languageOf α R
a2_right : (head✝ :: tail✝).join = cs
⊢ (head✝ :: tail✝).join = [] ∨
    ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (head✝ :: tail✝).join
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = [].join
Tactic:
case nil =>
  left
  simp
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_left : ∀ r ∈ hd :: tl, r ∈ RegExp.languageOf α R
a2_right : (hd :: tl).join = cs
⊢ (hd :: tl).join = [] ∨
    ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
case cons hd tl =>
  right
  simp at a2_left
  cases a2_left
  case _ a2_left_left a2_left_right =>
    apply Exists.intro hd
    tauto
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = [].join
Tactic:
left
Proof state after:
case h
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = []
Theorem: equiv_language_of_closure
Proof state before:
case h
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = []
Tactic:
simp
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_left : ∀ r ∈ hd :: tl, r ∈ RegExp.languageOf α R
a2_right : (hd :: tl).join = cs
⊢ (hd :: tl).join = [] ∨
    ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
right
Proof state after:
case h
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_left : ∀ r ∈ hd :: tl, r ∈ RegExp.languageOf α R
a2_right : (hd :: tl).join = cs
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Theorem: equiv_language_of_closure
Proof state before:
case h
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_left : ∀ r ∈ hd :: tl, r ∈ RegExp.languageOf α R
a2_right : (hd :: tl).join = cs
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
simp at a2_left
Proof state after:
case h
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left : hd ∈ RegExp.languageOf α R ∧ ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Theorem: equiv_language_of_closure
Proof state before:
case h
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left : hd ∈ RegExp.languageOf α R ∧ ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
cases a2_left
Proof state after:
case h.intro
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
left✝ : hd ∈ RegExp.languageOf α R
right✝ : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left_left : hd ∈ RegExp.languageOf α R
a2_left_right : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
case _ a2_left_left a2_left_right =>
  apply Exists.intro hd
  tauto
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left_left : hd ∈ RegExp.languageOf α R
a2_left_right : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
apply Exists.intro hd
Proof state after:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left_left : hd ∈ RegExp.languageOf α R
a2_left_right : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ hd ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ hd ++ a.join = (hd :: tl).join
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left_left : hd ∈ RegExp.languageOf α R
a2_left_right : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ hd ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ hd ++ a.join = (hd :: tl).join
Tactic:
tauto
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
case h.mpr
α : Type
R : RegExp α
cs : List α
⊢ (cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs) →
    ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
intro a1
Proof state after:
case h.mpr
α : Type
R : RegExp α
cs : List α
a1 : cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Theorem: equiv_language_of_closure
Proof state before:
case h.mpr
α : Type
R : RegExp α
cs : List α
a1 : cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
cases a1
Proof state after:
case h.mpr.inl
α : Type
R : RegExp α
cs : List α
h✝ : cs = []
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

case h.mpr.inr
α : Type
R : RegExp α
cs : List α
h✝ : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
case _ left =>
  apply Exists.intro []
  simp
  simp only [left]
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
case _ right =>
  apply Exists.elim right
  intro xs a2
  clear right
  cases a2
  case _ a2_left a2_right =>
    apply Exists.elim a2_right
    intro ys a3
    clear a2_right
    cases a3
    case _ a3_left a3_right =>
      apply Exists.intro ([xs] ++ ys)
      simp
      tauto
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
apply Exists.intro []
Proof state after:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ (∀ r ∈ [], r ∈ RegExp.languageOf α R) ∧ [].join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ (∀ r ∈ [], r ∈ RegExp.languageOf α R) ∧ [].join = cs
Tactic:
simp
Proof state after:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ [] = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ [] = cs
Tactic:
simp only [left]
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
apply Exists.elim right
Proof state after:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∀ (a : List α),
    (a ∈ RegExp.languageOf α R ∧ ∃ a_1, (∀ r ∈ a_1, r ∈ RegExp.languageOf α R) ∧ a ++ a_1.join = cs) →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∀ (a : List α),
    (a ∈ RegExp.languageOf α R ∧ ∃ a_1, (∀ r ∈ a_1, r ∈ RegExp.languageOf α R) ∧ a ++ a_1.join = cs) →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
intro xs a2
Proof state after:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
xs : List α
a2 : xs ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
xs : List α
a2 : xs ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
clear right
Proof state after:
α : Type
R : RegExp α
cs xs : List α
a2 : xs ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs xs : List α
a2 : xs ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
cases a2
Proof state after:
case intro
α : Type
R : RegExp α
cs xs : List α
left✝ : xs ∈ RegExp.languageOf α R
right✝ : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
case _ a2_left a2_right =>
  apply Exists.elim a2_right
  intro ys a3
  clear a2_right
  cases a3
  case _ a3_left a3_right =>
    apply Exists.intro ([xs] ++ ys)
    simp
    tauto
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
apply Exists.elim a2_right
Proof state after:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∀ (a : List (List α)),
    (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∀ (a : List (List α)),
    (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
intro ys a3
Proof state after:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
clear a2_right
Proof state after:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
cases a3
Proof state after:
case intro
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
left✝ : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
right✝ : xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
case _ a3_left a3_right =>
  apply Exists.intro ([xs] ++ ys)
  simp
  tauto
Proof state after:
no goals
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
apply Exists.intro ([xs] ++ ys)
Proof state after:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ (∀ r ∈ [xs] ++ ys, r ∈ RegExp.languageOf α R) ∧ ([xs] ++ ys).join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ (∀ r ∈ [xs] ++ ys, r ∈ RegExp.languageOf α R) ∧ ([xs] ++ ys).join = cs
Tactic:
simp
Proof state after:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ (xs ∈ RegExp.languageOf α R ∧ ∀ a ∈ ys, a ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
Theorem: equiv_language_of_closure
Proof state before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ (xs ∈ RegExp.languageOf α R ∧ ∀ a ∈ ys, a ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
F F' : Formula
v u : VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders F
h2 : Rec.fastReplaceFree v u F = F'
⊢ IsSub F v u F'
Tactic:
subst h2
Proof state after:
F : Formula
v u : VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders F
⊢ IsSub F v u (Rec.fastReplaceFree v u F)
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
X : PredName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (pred_var_ X xs) v u (pred_var_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
case pred_const_ X xs | pred_var_ X xs =>
  first | apply IsSub.pred_const_ | apply IsSub.pred_var_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v = x ∨ v = y → u ∉ binders
⊢ IsSub (eq_ x y) v u (eq_ (if v = x then u else x) (if v = y then u else y))
Tactic:
case eq_ x y =>
  apply IsSub.eq_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
binders : Finset VarName
h1 : True
⊢ IsSub false_ v u false_
Tactic:
case true_ | false_ =>
  first | apply IsSub.true_ | apply IsSub.false_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders phi
⊢ IsSub phi.not_ v u (Rec.fastReplaceFree v u phi).not_
Tactic:
case not_ phi phi_ih =>
  apply IsSub.not_
  exact phi_ih binders h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (def_ X xs) v u (def_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
case def_ X xs =>
  apply IsSub.def_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders (def_ a✝¹ a✝)
⊢ IsSub (def_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (def_ a✝¹ a✝))
Tactic:
simp only [Rec.fastAdmitsAux] at h1
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ → u ∉ binders
⊢ IsSub (def_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (def_ a✝¹ a✝))
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ → u ∉ binders
⊢ IsSub (def_ a✝¹ a✝) v u (Rec.fastReplaceFree v u (def_ a✝¹ a✝))
Tactic:
simp only [Rec.fastReplaceFree]
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ → u ∉ binders
⊢ IsSub (def_ a✝¹ a✝) v u (def_ a✝¹ (List.map (fun x => if v = x then u else x) a✝))
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
X : PredName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (pred_var_ X xs) v u (pred_var_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
first | apply IsSub.pred_const_ | apply IsSub.pred_var_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
X : PredName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (pred_const_ X xs) v u (pred_const_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
apply IsSub.pred_const_
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.fastAdmitsAux_and_fastReplaceFree_imp_isFreeSub
Proof state before:
v u : VarName
X : PredName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (pred_var_ X xs) v u (pred_var_ X (List.map (fun x => if v = x then u else x) xs))
Tactic:
apply IsSub.pred_var_
Proof state after:
no goals