internlm/Lean-Github huggingface dataset:
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
⊢ ∀ (a : ℕ), xs ∈ exp L a → xs ++ ys ∈ ⋃ n, exp L n
Tactic:
intro n a2
Proof state after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ ⋃ n, exp L n
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ ⋃ n, exp L n
Tactic:
clear ih_3
Proof state after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ ⋃ n, exp L n
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ ⋃ n, exp L n
Tactic:
simp
Proof state after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ i, xs ++ ys ∈ exp L i
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ i, xs ++ ys ∈ exp L i
Tactic:
apply Exists.intro (n + 1)
Proof state after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ exp L (n + 1)
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ exp L (n + 1)
Tactic:
simp only [exp]
Proof state after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ concat (exp L n) L
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ concat (exp L n) L
Tactic:
simp only [concat]
Proof state after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ {x | ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = x}
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ {x | ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = x}
Tactic:
simp
Proof state after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = xs ++ ys
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = xs ++ ys
Tactic:
apply Exists.intro xs
Proof state after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ∈ exp L n ∧ ∃ t ∈ L, xs ++ t = xs ++ ys
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ∈ exp L n ∧ ∃ t ∈ L, xs ++ t = xs ++ ys
Tactic:
constructor
Proof state after:
case left
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ∈ exp L n

case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ t ∈ L, xs ++ t = xs ++ ys
Theorem: Languages.thm_5_right
Proof state before:
case left
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ∈ exp L n
Tactic:
exact a2
Proof state after:
no goals
Theorem: Languages.thm_5_right
Proof state before:
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ t ∈ L, xs ++ t = xs ++ ys
Tactic:
apply Exists.intro ys
Proof state after:
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ys ∈ L ∧ xs ++ ys = xs ++ ys
Theorem: Languages.thm_5_right
Proof state before:
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ys ∈ L ∧ xs ++ ys = xs ++ ys
Tactic:
simp
Proof state after:
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ys ∈ L
Theorem: Languages.thm_5_right
Proof state before:
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ys ∈ L
Tactic:
exact ih_2
Proof state after:
no goals
Theorem: Languages.thm_5
Proof state before:
α : Type
L : Language α
⊢ kleene_closure α L = ⋃ n, exp L n
Tactic:
apply Set.eq_of_subset_of_subset
Proof state after:
case a
α : Type
L : Language α
⊢ kleene_closure α L ⊆ ⋃ n, exp L n

case a
α : Type
L : Language α
⊢ ⋃ n, exp L n ⊆ kleene_closure α L
Theorem: Languages.thm_5
Proof state before:
case a
α : Type
L : Language α
⊢ kleene_closure α L ⊆ ⋃ n, exp L n
Tactic:
exact thm_5_right L
Proof state after:
no goals
Theorem: Languages.thm_5
Proof state before:
case a
α : Type
L : Language α
⊢ ⋃ n, exp L n ⊆ kleene_closure α L
Tactic:
exact thm_5_left L
Proof state after:
no goals
Theorem: Languages.concat_exp_comm
Proof state before:
α : Type
L : Language α
n : ℕ
⊢ concat (exp L n) L = concat L (exp L n)
Tactic:
induction n
Proof state after:
case zero
α : Type
L : Language α
⊢ concat (exp L 0) L = concat L (exp L 0)

case succ
α : Type
L : Language α
n✝ : ℕ
a✝ : concat (exp L n✝) L = concat L (exp L n✝)
⊢ concat (exp L (n✝ + 1)) L = concat L (exp L (n✝ + 1))
Theorem: Languages.concat_exp_comm
Proof state before:
α : Type
L : Language α
⊢ concat (exp L 0) L = concat L (exp L 0)
Tactic:
case zero =>
  simp only [exp]
  simp only [concat]
  simp
Proof state after:
no goals
Theorem: Languages.concat_exp_comm
Proof state before:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (exp L (k + 1)) L = concat L (exp L (k + 1))
Tactic:
case succ k ih =>
  simp only [exp]
  conv => left; simp only [ih]
  simp only [thm_3_c]
Proof state after:
no goals
Theorem: Languages.concat_exp_comm
Proof state before:
α : Type
L : Language α
⊢ concat (exp L 0) L = concat L (exp L 0)
Tactic:
simp only [exp]
Proof state after:
α : Type
L : Language α
⊢ concat {[]} L = concat L {[]}
Theorem: Languages.concat_exp_comm
Proof state before:
α : Type
L : Language α
⊢ concat {[]} L = concat L {[]}
Tactic:
simp only [concat]
Proof state after:
α : Type
L : Language α
⊢ {x | ∃ s ∈ {[]}, ∃ t ∈ L, s ++ t = x} = {x | ∃ s ∈ L, ∃ t ∈ {[]}, s ++ t = x}
Theorem: Languages.concat_exp_comm
Proof state before:
α : Type
L : Language α
⊢ {x | ∃ s ∈ {[]}, ∃ t ∈ L, s ++ t = x} = {x | ∃ s ∈ L, ∃ t ∈ {[]}, s ++ t = x}
Tactic:
simp
Proof state after:
no goals
Theorem: Languages.concat_exp_comm
Proof state before:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (exp L (k + 1)) L = concat L (exp L (k + 1))
Tactic:
simp only [exp]
Proof state after:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (concat (exp L k) L) L = concat L (concat (exp L k) L)
Theorem: Languages.concat_exp_comm
Proof state before:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (concat (exp L k) L) L = concat L (concat (exp L k) L)
Tactic:
conv => left; simp only [ih]
Proof state after:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (concat L (exp L k)) L = concat L (concat (exp L k) L)
Theorem: Languages.concat_exp_comm
Proof state before:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (concat L (exp L k)) L = concat L (concat (exp L k) L)
Tactic:
simp only [thm_3_c]
Proof state after:
no goals
Theorem: Languages.thm_6
Proof state before:
α : Type
L : Language α
⊢ kleene_closure α L = {[]} ∪ concat L (kleene_closure α L)
Tactic:
apply Set.eq_of_subset_of_subset
Proof state after:
case a
α : Type
L : Language α
⊢ kleene_closure α L ⊆ {[]} ∪ concat L (kleene_closure α L)

case a
α : Type
L : Language α
⊢ {[]} ∪ concat L (kleene_closure α L) ⊆ kleene_closure α L
Theorem: Languages.thm_6
Proof state before:
case a
α : Type
L : Language α
⊢ kleene_closure α L ⊆ {[]} ∪ concat L (kleene_closure α L)
Tactic:
simp only [Set.subset_def]
Proof state after:
case a
α : Type
L : Language α
⊢ ∀ x ∈ kleene_closure α L, x ∈ {[]} ∪ concat L (kleene_closure α L)
Theorem: Languages.thm_6
Proof state before:
case a
α : Type
L : Language α
⊢ ∀ x ∈ kleene_closure α L, x ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
intro s a1
Proof state after:
case a
α : Type
L : Language α
s : Str α
a1 : s ∈ kleene_closure α L
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Theorem: Languages.thm_6
Proof state before:
case a
α : Type
L : Language α
s : Str α
a1 : s ∈ kleene_closure α L
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
simp only [thm_5 L] at a1
Proof state after:
case a
α : Type
L : Language α
s : Str α
a1 : s ∈ ⋃ n, exp L n
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Theorem: Languages.thm_6
Proof state before:
case a
α : Type
L : Language α
s : Str α
a1 : s ∈ ⋃ n, exp L n
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
simp at a1
Proof state after:
case a
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Theorem: Languages.thm_6
Proof state before:
case a
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
cases a1
Proof state after:
case a.intro
α : Type
L : Language α
s : Str α
w✝ : ℕ
h✝ : s ∈ exp L w✝
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Theorem: Languages.thm_6
Proof state before:
α : Type
L : Language α
s : Str α
i : ℕ
a2 : s ∈ exp L i
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
case _ i a2 =>
  simp
  sorry
Proof state after:
no goals
Theorem: Languages.thm_6
Proof state before:
α : Type
L : Language α
s : Str α
i : ℕ
a2 : s ∈ exp L i
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
simp
Proof state after:
α : Type
L : Language α
s : Str α
i : ℕ
a2 : s ∈ exp L i
⊢ s = [] ∨ s ∈ concat L (kleene_closure α L)
Theorem: Languages.thm_6
Proof state before:
α : Type
L : Language α
s : Str α
i : ℕ
a2 : s ∈ exp L i
⊢ s = [] ∨ s ∈ concat L (kleene_closure α L)
Tactic:
sorry
Proof state after:
no goals
Theorem: Languages.thm_6
Proof state before:
case a
α : Type
L : Language α
⊢ {[]} ∪ concat L (kleene_closure α L) ⊆ kleene_closure α L
Tactic:
simp only [Set.subset_def]
Proof state after:
case a
α : Type
L : Language α
⊢ ∀ x ∈ {[]} ∪ concat L (kleene_closure α L), x ∈ kleene_closure α L
Theorem: Languages.thm_6
Proof state before:
case a
α : Type
L : Language α
⊢ ∀ x ∈ {[]} ∪ concat L (kleene_closure α L), x ∈ kleene_closure α L
Tactic:
intro x a1
Proof state after:
case a
α : Type
L : Language α
x : Str α
a1 : x ∈ {[]} ∪ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Theorem: Languages.thm_6
Proof state before:
case a
α : Type
L : Language α
x : Str α
a1 : x ∈ {[]} ∪ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Tactic:
simp at a1
Proof state after:
case a
α : Type
L : Language α
x : Str α
a1 : x = [] ∨ x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Theorem: Languages.thm_6
Proof state before:
case a
α : Type
L : Language α
x : Str α
a1 : x = [] ∨ x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Tactic:
cases a1
Proof state after:
case a.inl
α : Type
L : Language α
x : Str α
h✝ : x = []
⊢ x ∈ kleene_closure α L

case a.inr
α : Type
L : Language α
x : Str α
h✝ : x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Theorem: Languages.thm_6
Proof state before:
α : Type
L : Language α
x : Str α
a1_left : x = []
⊢ x ∈ kleene_closure α L
Tactic:
case _ a1_left =>
  simp only [a1_left]
  exact kleene_closure.eps L
Proof state after:
no goals
Theorem: Languages.thm_6
Proof state before:
α : Type
L : Language α
x : Str α
a1_right : x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Tactic:
case _ a1_right =>
  simp only [thm_5 L] at a1_right
  sorry
Proof state after:
no goals
Theorem: Languages.thm_6
Proof state before:
α : Type
L : Language α
x : Str α
a1_left : x = []
⊢ x ∈ kleene_closure α L
Tactic:
simp only [a1_left]
Proof state after:
α : Type
L : Language α
x : Str α
a1_left : x = []
⊢ [] ∈ kleene_closure α L
Theorem: Languages.thm_6
Proof state before:
α : Type
L : Language α
x : Str α
a1_left : x = []
⊢ [] ∈ kleene_closure α L
Tactic:
exact kleene_closure.eps L
Proof state after:
no goals
Theorem: Languages.thm_6
Proof state before:
α : Type
L : Language α
x : Str α
a1_right : x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Tactic:
simp only [thm_5 L] at a1_right
Proof state after:
α : Type
L : Language α
x : Str α
a1_right : x ∈ concat L (⋃ n, exp L n)
⊢ x ∈ kleene_closure α L
Theorem: Languages.thm_6
Proof state before:
α : Type
L : Language α
x : Str α
a1_right : x ∈ concat L (⋃ n, exp L n)
⊢ x ∈ kleene_closure α L
Tactic:
sorry
Proof state after:
no goals
Theorem: LN.lc_at_zero_iff_is_free
Proof state before:
v : Var
⊢ Var.lc_at 0 v ↔ v.isFree
Tactic:
cases v
Proof state after:
case free_
a✝ : String
⊢ Var.lc_at 0 (free_ a✝) ↔ (free_ a✝).isFree

case bound_
a✝ : ℕ
⊢ Var.lc_at 0 (bound_ a✝) ↔ (bound_ a✝).isFree
Theorem: LN.lc_at_zero_iff_is_free
Proof state before:
x : String
⊢ Var.lc_at 0 (free_ x) ↔ (free_ x).isFree
Tactic:
case free_ x =>
  simp only [Var.lc_at]
  simp only [isFree]
Proof state after:
no goals
Theorem: LN.lc_at_zero_iff_is_free
Proof state before:
i : ℕ
⊢ Var.lc_at 0 (bound_ i) ↔ (bound_ i).isFree
Tactic:
case bound_ i =>
  simp only [Var.lc_at]
  simp only [isFree]
  simp
Proof state after:
no goals
Theorem: LN.lc_at_zero_iff_is_free
Proof state before:
x : String
⊢ Var.lc_at 0 (free_ x) ↔ (free_ x).isFree
Tactic:
simp only [Var.lc_at]
Proof state after:
x : String
⊢ True ↔ (free_ x).isFree
Theorem: LN.lc_at_zero_iff_is_free
Proof state before:
x : String
⊢ True ↔ (free_ x).isFree
Tactic:
simp only [isFree]
Proof state after:
no goals
Theorem: LN.lc_at_zero_iff_is_free
Proof state before:
i : ℕ
⊢ Var.lc_at 0 (bound_ i) ↔ (bound_ i).isFree
Tactic:
simp only [Var.lc_at]
Proof state after:
i : ℕ
⊢ i < 0 ↔ (bound_ i).isFree
Theorem: LN.lc_at_zero_iff_is_free
Proof state before:
i : ℕ
⊢ i < 0 ↔ (bound_ i).isFree
Tactic:
simp only [isFree]
Proof state after:
i : ℕ
⊢ i < 0 ↔ False
Theorem: LN.lc_at_zero_iff_is_free
Proof state before:
i : ℕ
⊢ i < 0 ↔ False
Tactic:
simp
Proof state after:
no goals
Theorem: LN.free_var_list_to_string_list
Proof state before:
vs : List Var
h1 : ∀ v ∈ vs, Var.lc_at 0 v
⊢ ∃ xs, vs = List.map free_ xs
Tactic:
induction vs
Proof state after:
case nil
h1 : ∀ v ∈ [], Var.lc_at 0 v
⊢ ∃ xs, [] = List.map free_ xs

case cons
head✝ : Var
tail✝ : List Var
tail_ih✝ : (∀ v ∈ tail✝, Var.lc_at 0 v) → ∃ xs, tail✝ = List.map free_ xs
h1 : ∀ v ∈ head✝ :: tail✝, Var.lc_at 0 v
⊢ ∃ xs, head✝ :: tail✝ = List.map free_ xs
Theorem: LN.free_var_list_to_string_list
Proof state before:
h1 : ∀ v ∈ [], Var.lc_at 0 v
⊢ ∃ xs, [] = List.map free_ xs
Tactic:
case nil =>
  apply Exists.intro []
  simp
Proof state after:
no goals
Theorem: LN.free_var_list_to_string_list
Proof state before:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1 : ∀ v ∈ hd :: tl, Var.lc_at 0 v
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
case cons hd tl ih =>
  simp at h1
  cases h1
  case intro h1_left h1_right =>
    specialize ih h1_right
    apply Exists.elim ih
    intro xs a1
    cases hd
    case free_ x =>
      apply Exists.intro (x :: xs)
      simp
      exact a1
    case bound_ i =>
      simp only [Var.lc_at] at h1_left
      simp at h1_left
Proof state after:
no goals
Theorem: LN.free_var_list_to_string_list
Proof state before:
h1 : ∀ v ∈ [], Var.lc_at 0 v
⊢ ∃ xs, [] = List.map free_ xs
Tactic:
apply Exists.intro []
Proof state after:
h1 : ∀ v ∈ [], Var.lc_at 0 v
⊢ [] = List.map free_ []
Theorem: LN.free_var_list_to_string_list
Proof state before:
h1 : ∀ v ∈ [], Var.lc_at 0 v
⊢ [] = List.map free_ []
Tactic:
simp
Proof state after:
no goals
Theorem: LN.free_var_list_to_string_list
Proof state before:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1 : ∀ v ∈ hd :: tl, Var.lc_at 0 v
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
simp at h1
Proof state after:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1 : Var.lc_at 0 hd ∧ ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs
Theorem: LN.free_var_list_to_string_list
Proof state before:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1 : Var.lc_at 0 hd ∧ ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
cases h1
Proof state after:
case intro
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
left✝ : Var.lc_at 0 hd
right✝ : ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs
Theorem: LN.free_var_list_to_string_list
Proof state before:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
case intro h1_left h1_right =>
  specialize ih h1_right
  apply Exists.elim ih
  intro xs a1
  cases hd
  case free_ x =>
    apply Exists.intro (x :: xs)
    simp
    exact a1
  case bound_ i =>
    simp only [Var.lc_at] at h1_left
    simp at h1_left
Proof state after:
no goals
Theorem: LN.free_var_list_to_string_list
Proof state before:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
specialize ih h1_right
Proof state after:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
⊢ ∃ xs, hd :: tl = List.map free_ xs
Theorem: LN.free_var_list_to_string_list
Proof state before:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
apply Exists.elim ih
Proof state after:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
⊢ ∀ (a : List String), tl = List.map free_ a → ∃ xs, hd :: tl = List.map free_ xs
Theorem: LN.free_var_list_to_string_list
Proof state before:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
⊢ ∀ (a : List String), tl = List.map free_ a → ∃ xs, hd :: tl = List.map free_ xs
Tactic:
intro xs a1
Proof state after:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
⊢ ∃ xs, hd :: tl = List.map free_ xs
Theorem: LN.free_var_list_to_string_list
Proof state before:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
cases hd
Proof state after:
case free_
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
a✝ : String
h1_left : Var.lc_at 0 (free_ a✝)
⊢ ∃ xs, free_ a✝ :: tl = List.map free_ xs

case bound_
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
a✝ : ℕ
h1_left : Var.lc_at 0 (bound_ a✝)
⊢ ∃ xs, bound_ a✝ :: tl = List.map free_ xs
Theorem: LN.free_var_list_to_string_list
Proof state before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ ∃ xs, free_ x :: tl = List.map free_ xs
Tactic:
case free_ x =>
  apply Exists.intro (x :: xs)
  simp
  exact a1
Proof state after:
no goals
Theorem: LN.free_var_list_to_string_list
Proof state before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
i : ℕ
h1_left : Var.lc_at 0 (bound_ i)
⊢ ∃ xs, bound_ i :: tl = List.map free_ xs
Tactic:
case bound_ i =>
  simp only [Var.lc_at] at h1_left
  simp at h1_left
Proof state after:
no goals
Theorem: LN.free_var_list_to_string_list
Proof state before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ ∃ xs, free_ x :: tl = List.map free_ xs
Tactic:
apply Exists.intro (x :: xs)
Proof state after:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ free_ x :: tl = List.map free_ (x :: xs)
Theorem: LN.free_var_list_to_string_list
Proof state before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ free_ x :: tl = List.map free_ (x :: xs)
Tactic:
simp
Proof state after:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ tl = List.map free_ xs
Theorem: LN.free_var_list_to_string_list
Proof state before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ tl = List.map free_ xs
Tactic:
exact a1
Proof state after:
no goals
Theorem: LN.free_var_list_to_string_list
Proof state before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
i : ℕ
h1_left : Var.lc_at 0 (bound_ i)
⊢ ∃ xs, bound_ i :: tl = List.map free_ xs
Tactic:
simp only [Var.lc_at] at h1_left
Proof state after:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
i : ℕ
h1_left : i < 0
⊢ ∃ xs, bound_ i :: tl = List.map free_ xs
Theorem: LN.free_var_list_to_string_list
Proof state before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
i : ℕ
h1_left : i < 0
⊢ ∃ xs, bound_ i :: tl = List.map free_ xs
Tactic:
simp at h1_left
Proof state after:
no goals
Theorem: LN.VarOpenFreeVarSet
Proof state before:
j : ℕ
z : String
v : Var
⊢ (Var.open j (free_ z) v).freeVarSet ⊆ v.freeVarSet ∪ {free_ z}
Tactic:
cases v
Proof state after:
case free_
j : ℕ
z a✝ : String
⊢ (Var.open j (free_ z) (free_ a✝)).freeVarSet ⊆ (free_ a✝).freeVarSet ∪ {free_ z}

case bound_
j : ℕ
z : String
a✝ : ℕ
⊢ (Var.open j (free_ z) (bound_ a✝)).freeVarSet ⊆ (bound_ a✝).freeVarSet ∪ {free_ z}
Theorem: LN.VarOpenFreeVarSet
Proof state before:
j : ℕ
z x : String
⊢ (Var.open j (free_ z) (free_ x)).freeVarSet ⊆ (free_ x).freeVarSet ∪ {free_ z}
Tactic:
case free_ x =>
  simp only [Var.open]
  simp only [Var.freeVarSet]
  simp
Proof state after:
no goals
Theorem: LN.VarOpenFreeVarSet
Proof state before:
j : ℕ
z : String
i : ℕ
⊢ (Var.open j (free_ z) (bound_ i)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ {free_ z}
Tactic:
case bound_ i =>
  simp only [Var.open]
  split_ifs
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 c2 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 c2 =>
    simp only [Var.freeVarSet]
    simp
Proof state after:
no goals
Theorem: LN.VarOpenFreeVarSet
Proof state before:
j : ℕ
z x : String
⊢ (Var.open j (free_ z) (free_ x)).freeVarSet ⊆ (free_ x).freeVarSet ∪ {free_ z}
Tactic:
simp only [Var.open]
Proof state after:
j : ℕ
z x : String
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet ∪ {free_ z}
Theorem: LN.VarOpenFreeVarSet
Proof state before:
j : ℕ
z x : String
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet ∪ {free_ z}
Tactic:
simp only [Var.freeVarSet]
Proof state after:
j : ℕ
z x : String
⊢ {free_ x} ⊆ {free_ x} ∪ {free_ z}