internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
c3 : h1_v = x
⊢ V h1_t = V h1_t
Tactic:
simp only [if_pos c3]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
c3 : ¬h1_v = x
⊢ V x = V x
Tactic:
simp only [if_neg c3]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ v' ∈ hd.args
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
Proof state after:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args
Tactic:
simp only [← List.mem_toFinset]
Proof state after:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args.toFinset
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args.toFinset
Tactic:
apply Finset.mem_of_subset hd.h1 a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h1.h2
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ hd.args.length = (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs).length
Tactic:
simp
Proof state after:
case h1.h2
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ hd.args.length = h1_xs.length
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h1.h2
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ hd.args.length = h1_xs.length
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : ¬(h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length)
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
simp only [List.length_map] at c2
Proof state after:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q
Tactic:
simp at c2
Proof state after:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
c2 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
c2 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
c2 : ¬(h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length)
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
exact ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_is_valid
Proof state before:
v t : VarName
F F' : Formula
h1 : IsSub F v t F'
h2 : F.IsValid
⊢ F'.IsValid
Tactic:
simp only [IsValid] at h2
Proof state after:
v t : VarName
F F' : Formula
h1 : IsSub F v t F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ F'.IsValid
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_is_valid
Proof state before:
v t : VarName
F F' : Formula
h1 : IsSub F v t F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ F'.IsValid
Tactic:
simp only [IsValid]
Proof state after:
v t : VarName
F F' : Formula
h1 : IsSub F v t F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_is_valid
Proof state before:
v t : VarName
F F' : Formula
h1 : IsSub F v t F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F'
Tactic:
intro D I V E
Proof state after:
v t : VarName
F F' : Formula
h1 : IsSub F v t F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E F'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_is_valid
Proof state before:
v t : VarName
F F' : Formula
h1 : IsSub F v t F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E F'
Tactic:
simp only [← substitution_theorem D I V E v t F F' h1]
Proof state after:
v t : VarName
F F' : Formula
h1 : IsSub F v t F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I (Function.updateITE V v (V t)) E F
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_is_valid
Proof state before:
v t : VarName
F F' : Formula
h1 : IsSub F v t F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I (Function.updateITE V v (V t)) E F
Tactic:
apply h2
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
e : RegExp α
⊢ e.is_nullable ↔ [] ∈ RegExp.languageOf α e
Tactic:
induction e
Proof state after:
case char
α : Type
a✝ : α
⊢ (RegExp.char a✝).is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.char a✝)

case epsilon
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.epsilon

case zero
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.zero

case union
α : Type
a✝¹ a✝ : RegExp α
a_ih✝¹ : a✝¹.is_nullable ↔ [] ∈ RegExp.languageOf α a✝¹
a_ih✝ : a✝.is_nullable ↔ [] ∈ RegExp.languageOf α a✝
⊢ (a✝¹.union a✝).is_nullable ↔ [] ∈ RegExp.languageOf α (a✝¹.union a✝)

case concat
α : Type
a✝¹ a✝ : RegExp α
a_ih✝¹ : a✝¹.is_nullable ↔ [] ∈ RegExp.languageOf α a✝¹
a_ih✝ : a✝.is_nullable ↔ [] ∈ RegExp.languageOf α a✝
⊢ (a✝¹.concat a✝).is_nullable ↔ [] ∈ RegExp.languageOf α (a✝¹.concat a✝)

case closure
α : Type
a✝ : RegExp α
a_ih✝ : a✝.is_nullable ↔ [] ∈ RegExp.languageOf α a✝
⊢ a✝.closure.is_nullable ↔ [] ∈ RegExp.languageOf α a✝.closure
Theorem: is_nullable_def
Proof state before:
α : Type
a : α
⊢ (RegExp.char a).is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.char a)
Tactic:
case char a =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.epsilon
Tactic:
case epsilon =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.zero
Tactic:
case zero =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.union s).is_nullable ↔ [] ∈ RegExp.languageOf α (r.union s)
Tactic:
case union r s r_ih s_ih =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
  simp only [r_ih]
  simp only [s_ih]
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.concat s).is_nullable ↔ [] ∈ RegExp.languageOf α (r.concat s)
Tactic:
case concat r s r_ih s_ih =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
  simp only [r_ih]
  simp only [s_ih]
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔ [] ∈ RegExp.languageOf α e.closure
Tactic:
case closure e _ =>
  simp only [equiv_language_of_closure]
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
a : α
⊢ (RegExp.char a).is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.char a)
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
a : α
⊢ (RegExp.char a).is_nullable ↔ [] ∈ {[a]}
Theorem: is_nullable_def
Proof state before:
α : Type
a : α
⊢ (RegExp.char a).is_nullable ↔ [] ∈ {[a]}
Tactic:
simp only [RegExp.is_nullable]
Proof state after:
α : Type
a : α
⊢ False ↔ [] ∈ {[a]}
Theorem: is_nullable_def
Proof state before:
α : Type
a : α
⊢ False ↔ [] ∈ {[a]}
Tactic:
simp
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.epsilon
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ {[]}
Theorem: is_nullable_def
Proof state before:
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ {[]}
Tactic:
simp only [RegExp.is_nullable]
Proof state after:
α : Type
⊢ True ↔ [] ∈ {[]}
Theorem: is_nullable_def
Proof state before:
α : Type
⊢ True ↔ [] ∈ {[]}
Tactic:
simp
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ ∅
Theorem: is_nullable_def
Proof state before:
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ ∅
Tactic:
simp only [RegExp.is_nullable]
Proof state after:
α : Type
⊢ False ↔ [] ∈ ∅
Theorem: is_nullable_def
Proof state before:
α : Type
⊢ False ↔ [] ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.union s).is_nullable ↔ [] ∈ RegExp.languageOf α (r.union s)
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.union s).is_nullable ↔ [] ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.union s).is_nullable ↔ [] ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Tactic:
simp only [RegExp.is_nullable]
Proof state after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Tactic:
simp
Proof state after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∨ [] ∈ RegExp.languageOf α s
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∨ [] ∈ RegExp.languageOf α s
Tactic:
simp only [r_ih]
Proof state after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ [] ∈ RegExp.languageOf α r ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∨ [] ∈ RegExp.languageOf α s
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ [] ∈ RegExp.languageOf α r ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∨ [] ∈ RegExp.languageOf α s
Tactic:
simp only [s_ih]
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.concat s).is_nullable ↔ [] ∈ RegExp.languageOf α (r.concat s)
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.concat s).is_nullable ↔ [] ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = x}
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.concat s).is_nullable ↔ [] ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = x}
Tactic:
simp only [RegExp.is_nullable]
Proof state after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∧ s.is_nullable ↔
    [] ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = x}
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∧ s.is_nullable ↔
    [] ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = x}
Tactic:
simp
Proof state after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∧ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∧ [] ∈ RegExp.languageOf α s
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∧ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∧ [] ∈ RegExp.languageOf α s
Tactic:
simp only [r_ih]
Proof state after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ [] ∈ RegExp.languageOf α r ∧ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∧ [] ∈ RegExp.languageOf α s