internlm/Lean-Github huggingface dataset:
Theorem: LN.HoldsClose
Proof state before:
case h
D : Type
I : Interpretation D
z x : String
phi : Formula
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
phi_ih :
  Holds D I (shift D V d) phi ↔
    Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi)
⊢ Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi) ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
Tactic:
congr! 1
Proof state after:
case h.a.h.e'_3
D : Type
I : Interpretation D
z x : String
phi : Formula
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
phi_ih :
  Holds D I (shift D V d) phi ↔
    Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi)
⊢ shift D V d ∘ Var.close (j + 1) (free_ z) = shift D (V ∘ Var.close j (free_ z)) d
Theorem: LN.HoldsClose
Proof state before:
case h.a.h.e'_3
D : Type
I : Interpretation D
z x : String
phi : Formula
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
phi_ih :
  Holds D I (shift D V d) phi ↔
    Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi)
⊢ shift D V d ∘ Var.close (j + 1) (free_ z) = shift D (V ∘ Var.close j (free_ z)) d
Tactic:
apply extracted_1
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
F : Formula
j : ℕ
zs : List String
h1 : lc_at j F
⊢ openList j (List.map free_ zs) F = F
Tactic:
induction F generalizing j
Proof state after:
case pred_
zs : List String
a✝¹ : String
a✝ : List Var
j : ℕ
h1 : lc_at j (pred_ a✝¹ a✝)
⊢ openList j (List.map free_ zs) (pred_ a✝¹ a✝) = pred_ a✝¹ a✝

case not_
zs : List String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), lc_at j a✝ → openList j (List.map free_ zs) a✝ = a✝
j : ℕ
h1 : lc_at j a✝.not_
⊢ openList j (List.map free_ zs) a✝.not_ = a✝.not_

case imp_
zs : List String
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (j : ℕ), lc_at j a✝¹ → openList j (List.map free_ zs) a✝¹ = a✝¹
a_ih✝ : ∀ (j : ℕ), lc_at j a✝ → openList j (List.map free_ zs) a✝ = a✝
j : ℕ
h1 : lc_at j (a✝¹.imp_ a✝)
⊢ openList j (List.map free_ zs) (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case forall_
zs : List String
a✝¹ : String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), lc_at j a✝ → openList j (List.map free_ zs) a✝ = a✝
j : ℕ
h1 : lc_at j (forall_ a✝¹ a✝)
⊢ openList j (List.map free_ zs) (forall_ a✝¹ a✝) = forall_ a✝¹ a✝
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : lc_at j (pred_ X vs)
⊢ openList j (List.map free_ zs) (pred_ X vs) = pred_ X vs
Tactic:
case pred_ X vs =>
  simp only [Formula.lc_at] at h1
  simp only [Formula.openList]
  simp
  apply List.map_mem_id
  intro v a1
  specialize h1 v a1
  cases v
  case _ x =>
    simp only [Var.openList]
  case _ i =>
    cases i
    case zero =>
      simp only [Var.lc_at] at h1
      simp only [Var.openList]
      simp only [if_pos h1]
    case succ i =>
      simp only [Var.lc_at] at h1
      simp only [Var.openList]
      simp only [if_pos h1]
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi.not_
⊢ openList j (List.map free_ zs) phi.not_ = phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.lc_at] at h1
  simp only [Formula.openList]
  congr!
  exact phi_ih j h1
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j (forall_ x phi)
⊢ openList j (List.map free_ zs) (forall_ x phi) = forall_ x phi
Tactic:
case forall_ x phi phi_ih =>
  simp only [Formula.lc_at] at h1
  simp only [Formula.openList]
  simp
  exact phi_ih (j + 1) h1
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : lc_at j (pred_ X vs)
⊢ openList j (List.map free_ zs) (pred_ X vs) = pred_ X vs
Tactic:
simp only [Formula.lc_at] at h1
Proof state after:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ openList j (List.map free_ zs) (pred_ X vs) = pred_ X vs
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ openList j (List.map free_ zs) (pred_ X vs) = pred_ X vs
Tactic:
simp only [Formula.openList]
Proof state after:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ pred_ X (List.map (Var.openList j (List.map free_ zs)) vs) = pred_ X vs
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ pred_ X (List.map (Var.openList j (List.map free_ zs)) vs) = pred_ X vs
Tactic:
simp
Proof state after:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map (Var.openList j (List.map free_ zs)) vs = vs
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map (Var.openList j (List.map free_ zs)) vs = vs
Tactic:
apply List.map_mem_id
Proof state after:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ ∀ x ∈ vs, Var.openList j (List.map free_ zs) x = x
Theorem: LN.Formula.OpenListLC
Proof state before:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ ∀ x ∈ vs, Var.openList j (List.map free_ zs) x = x
Tactic:
intro v a1
Proof state after:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
v : Var
a1 : v ∈ vs
⊢ Var.openList j (List.map free_ zs) v = v
Theorem: LN.Formula.OpenListLC
Proof state before:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
v : Var
a1 : v ∈ vs
⊢ Var.openList j (List.map free_ zs) v = v
Tactic:
specialize h1 v a1
Proof state after:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
h1 : Var.lc_at j v
⊢ Var.openList j (List.map free_ zs) v = v
Theorem: LN.Formula.OpenListLC
Proof state before:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
h1 : Var.lc_at j v
⊢ Var.openList j (List.map free_ zs) v = v
Tactic:
cases v
Proof state after:
case h1.free_
zs : List String
X : String
vs : List Var
j : ℕ
a✝ : String
a1 : free_ a✝ ∈ vs
h1 : Var.lc_at j (free_ a✝)
⊢ Var.openList j (List.map free_ zs) (free_ a✝) = free_ a✝

case h1.bound_
zs : List String
X : String
vs : List Var
j a✝ : ℕ
a1 : bound_ a✝ ∈ vs
h1 : Var.lc_at j (bound_ a✝)
⊢ Var.openList j (List.map free_ zs) (bound_ a✝) = bound_ a✝
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
x : String
a1 : free_ x ∈ vs
h1 : Var.lc_at j (free_ x)
⊢ Var.openList j (List.map free_ zs) (free_ x) = free_ x
Tactic:
case _ x =>
  simp only [Var.openList]
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ i ∈ vs
h1 : Var.lc_at j (bound_ i)
⊢ Var.openList j (List.map free_ zs) (bound_ i) = bound_ i
Tactic:
case _ i =>
  cases i
  case zero =>
    simp only [Var.lc_at] at h1
    simp only [Var.openList]
    simp only [if_pos h1]
  case succ i =>
    simp only [Var.lc_at] at h1
    simp only [Var.openList]
    simp only [if_pos h1]
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
x : String
a1 : free_ x ∈ vs
h1 : Var.lc_at j (free_ x)
⊢ Var.openList j (List.map free_ zs) (free_ x) = free_ x
Tactic:
simp only [Var.openList]
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ i ∈ vs
h1 : Var.lc_at j (bound_ i)
⊢ Var.openList j (List.map free_ zs) (bound_ i) = bound_ i
Tactic:
cases i
Proof state after:
case zero
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : Var.lc_at j (bound_ 0)
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0

case succ
zs : List String
X : String
vs : List Var
j n✝ : ℕ
a1 : bound_ (n✝ + 1) ∈ vs
h1 : Var.lc_at j (bound_ (n✝ + 1))
⊢ Var.openList j (List.map free_ zs) (bound_ (n✝ + 1)) = bound_ (n✝ + 1)
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : Var.lc_at j (bound_ 0)
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0
Tactic:
case zero =>
  simp only [Var.lc_at] at h1
  simp only [Var.openList]
  simp only [if_pos h1]
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : Var.lc_at j (bound_ (i + 1))
⊢ Var.openList j (List.map free_ zs) (bound_ (i + 1)) = bound_ (i + 1)
Tactic:
case succ i =>
  simp only [Var.lc_at] at h1
  simp only [Var.openList]
  simp only [if_pos h1]
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : Var.lc_at j (bound_ 0)
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0
Tactic:
simp only [Var.lc_at] at h1
Proof state after:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : 0 < j
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : 0 < j
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0
Tactic:
simp only [Var.openList]
Proof state after:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : 0 < j
⊢ (if 0 < j then bound_ 0
    else
      if x : 0 - j < (List.map free_ zs).length then (List.map free_ zs)[0 - j]
      else bound_ (0 - j - (List.map free_ zs).length + j)) =
    bound_ 0
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : 0 < j
⊢ (if 0 < j then bound_ 0
    else
      if x : 0 - j < (List.map free_ zs).length then (List.map free_ zs)[0 - j]
      else bound_ (0 - j - (List.map free_ zs).length + j)) =
    bound_ 0
Tactic:
simp only [if_pos h1]
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : Var.lc_at j (bound_ (i + 1))
⊢ Var.openList j (List.map free_ zs) (bound_ (i + 1)) = bound_ (i + 1)
Tactic:
simp only [Var.lc_at] at h1
Proof state after:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : i + 1 < j
⊢ Var.openList j (List.map free_ zs) (bound_ (i + 1)) = bound_ (i + 1)
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : i + 1 < j
⊢ Var.openList j (List.map free_ zs) (bound_ (i + 1)) = bound_ (i + 1)
Tactic:
simp only [Var.openList]
Proof state after:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : i + 1 < j
⊢ (if i + 1 < j then bound_ (i + 1)
    else
      if x : i + 1 - j < (List.map free_ zs).length then (List.map free_ zs)[i + 1 - j]
      else bound_ (i + 1 - j - (List.map free_ zs).length + j)) =
    bound_ (i + 1)
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : i + 1 < j
⊢ (if i + 1 < j then bound_ (i + 1)
    else
      if x : i + 1 - j < (List.map free_ zs).length then (List.map free_ zs)[i + 1 - j]
      else bound_ (i + 1 - j - (List.map free_ zs).length + j)) =
    bound_ (i + 1)
Tactic:
simp only [if_pos h1]
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi.not_
⊢ openList j (List.map free_ zs) phi.not_ = phi.not_
Tactic:
simp only [Formula.lc_at] at h1
Proof state after:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ openList j (List.map free_ zs) phi.not_ = phi.not_
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ openList j (List.map free_ zs) phi.not_ = phi.not_
Tactic:
simp only [Formula.openList]
Proof state after:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ (openList j (List.map free_ zs) phi).not_ = phi.not_
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ (openList j (List.map free_ zs) phi).not_ = phi.not_
Tactic:
congr!
Proof state after:
case h.e'_1
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ openList j (List.map free_ zs) phi = phi
Theorem: LN.Formula.OpenListLC
Proof state before:
case h.e'_1
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ openList j (List.map free_ zs) phi = phi
Tactic:
exact phi_ih j h1
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1 : lc_at j (phi.imp_ psi)
⊢ openList j (List.map free_ zs) (phi.imp_ psi) = phi.imp_ psi
Tactic:
simp only [Formula.lc_at] at h1
Proof state after:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1 : lc_at j phi ∧ lc_at j psi
⊢ openList j (List.map free_ zs) (phi.imp_ psi) = phi.imp_ psi
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1 : lc_at j phi ∧ lc_at j psi
⊢ openList j (List.map free_ zs) (phi.imp_ psi) = phi.imp_ psi
Tactic:
simp only [Formula.openList]
Proof state after:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1 : lc_at j phi ∧ lc_at j psi
⊢ (openList j (List.map free_ zs) phi).imp_ (openList j (List.map free_ zs) psi) = phi.imp_ psi
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1 : lc_at j phi ∧ lc_at j psi
⊢ (openList j (List.map free_ zs) phi).imp_ (openList j (List.map free_ zs) psi) = phi.imp_ psi
Tactic:
cases h1
Proof state after:
case intro
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
left✝ : lc_at j phi
right✝ : lc_at j psi
⊢ (openList j (List.map free_ zs) phi).imp_ (openList j (List.map free_ zs) psi) = phi.imp_ psi
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ (openList j (List.map free_ zs) phi).imp_ (openList j (List.map free_ zs) psi) = phi.imp_ psi
Tactic:
congr!
Proof state after:
case h.e'_1
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ openList j (List.map free_ zs) phi = phi

case h.e'_2
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ openList j (List.map free_ zs) psi = psi
Theorem: LN.Formula.OpenListLC
Proof state before:
case h.e'_1
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ openList j (List.map free_ zs) phi = phi
Tactic:
exact phi_ih j h1_left
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
case h.e'_2
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ openList j (List.map free_ zs) psi = psi
Tactic:
exact psi_ih j h1_right
Proof state after:
no goals
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j (forall_ x phi)
⊢ openList j (List.map free_ zs) (forall_ x phi) = forall_ x phi
Tactic:
simp only [Formula.lc_at] at h1
Proof state after:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ openList j (List.map free_ zs) (forall_ x phi) = forall_ x phi
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ openList j (List.map free_ zs) (forall_ x phi) = forall_ x phi
Tactic:
simp only [Formula.openList]
Proof state after:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ forall_ x (openList (j + 1) (List.map free_ zs) phi) = forall_ x phi
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ forall_ x (openList (j + 1) (List.map free_ zs) phi) = forall_ x phi
Tactic:
simp
Proof state after:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ openList (j + 1) (List.map free_ zs) phi = phi
Theorem: LN.Formula.OpenListLC
Proof state before:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ openList (j + 1) (List.map free_ zs) phi = phi
Tactic:
exact phi_ih (j + 1) h1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
F : Formula
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) F) ↔ Formula.lc_at (j + zs.length) F
Tactic:
induction F generalizing j zs
Proof state after:
case pred_
a✝¹ : String
a✝ : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (pred_ a✝¹ a✝)) ↔ Formula.lc_at (j + zs.length) (pred_ a✝¹ a✝)

case not_
a✝ : Formula
a_ih✝ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝) ↔ Formula.lc_at (j + zs.length) a✝
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝.not_) ↔ Formula.lc_at (j + zs.length) a✝.not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝¹) ↔ Formula.lc_at (j + zs.length) a✝¹
a_ih✝ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝) ↔ Formula.lc_at (j + zs.length) a✝
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (a✝¹.imp_ a✝)) ↔ Formula.lc_at (j + zs.length) (a✝¹.imp_ a✝)

case forall_
a✝¹ : String
a✝ : Formula
a_ih✝ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝) ↔ Formula.lc_at (j + zs.length) a✝
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (forall_ a✝¹ a✝)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝¹ a✝)
Theorem: LN.lc_at_instantiate
Proof state before:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi.not_) ↔ Formula.lc_at (j + zs.length) phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.openList]
  simp only [Formula.lc_at]
  apply phi_ih
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (forall_ a✝ phi)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝ phi)
Tactic:
case forall_ _ phi phi_ih =>
  simp only [Formula.openList]
  simp only [Formula.lc_at]
  simp only [phi_ih]
  have s1 : j + 1 + List.length zs = j + List.length zs + 1
  linarith;
  simp only [s1]
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (pred_ X vs)) ↔ Formula.lc_at (j + zs.length) (pred_ X vs)
Tactic:
simp only [Formula.openList]
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (pred_ X (List.map (Var.openList j (List.map free_ zs)) vs)) ↔
    Formula.lc_at (j + zs.length) (pred_ X vs)
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (pred_ X (List.map (Var.openList j (List.map free_ zs)) vs)) ↔
    Formula.lc_at (j + zs.length) (pred_ X vs)
Tactic:
simp only [Formula.lc_at]
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
⊢ (∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v) ↔ ∀ v ∈ vs, Var.lc_at (j + zs.length) v
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
⊢ (∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v) ↔ ∀ v ∈ vs, Var.lc_at (j + zs.length) v
Tactic:
constructor
Proof state after:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
⊢ (∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v) → ∀ v ∈ vs, Var.lc_at (j + zs.length) v

case mpr
X : String
vs : List Var
j : ℕ
zs : List String
⊢ (∀ v ∈ vs, Var.lc_at (j + zs.length) v) → ∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v
Theorem: LN.lc_at_instantiate
Proof state before:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
⊢ (∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v) → ∀ v ∈ vs, Var.lc_at (j + zs.length) v
Tactic:
intro a1 v a2
Proof state after:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v
v : Var
a2 : v ∈ vs
⊢ Var.lc_at (j + zs.length) v
Theorem: LN.lc_at_instantiate
Proof state before:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v
v : Var
a2 : v ∈ vs
⊢ Var.lc_at (j + zs.length) v
Tactic:
specialize a1 (Var.openList j (List.map free_ zs) v)
Proof state after:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 :
  Var.openList j (List.map free_ zs) v ∈ List.map (Var.openList j (List.map free_ zs)) vs →
    Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v