internlm/Lean-Github huggingface dataset:
Theorem: LN.extracted_1
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
s1 : ¬i < j
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
simp only [if_neg s1]
Proof state after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
s1 : ¬i < j
⊢ shift D V d (bound_ (i + 1 + 1)) = V (bound_ (i + 1))
Theorem: LN.extracted_1
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
s1 : ¬i < j
⊢ shift D V d (bound_ (i + 1 + 1)) = V (bound_ (i + 1))
Tactic:
simp only [shift]
Proof state after:
no goals
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
z : String
F : Formula
j : ℕ
h1 : ¬occursIn (free_ z) F
h2 : Formula.lc_at j F
⊢ Holds D I V F ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] F)
Tactic:
induction F generalizing V j
Proof state after:
case pred_
D : Type
I : Interpretation D
z a✝¹ : String
a✝ : List Var
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (pred_ a✝¹ a✝)
h2 : Formula.lc_at j (pred_ a✝¹ a✝)
⊢ Holds D I V (pred_ a✝¹ a✝) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ a✝¹ a✝))

case not_
D : Type
I : Interpretation D
z : String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝ →
      Formula.lc_at j a✝ → (Holds D I V a✝ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) a✝.not_
h2 : Formula.lc_at j a✝.not_
⊢ Holds D I V a✝.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝.not_)

case imp_
D : Type
I : Interpretation D
z : String
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝¹ →
      Formula.lc_at j a✝¹ → (Holds D I V a✝¹ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝ →
      Formula.lc_at j a✝ → (Holds D I V a✝ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (a✝¹.imp_ a✝)
h2 : Formula.lc_at j (a✝¹.imp_ a✝)
⊢ Holds D I V (a✝¹.imp_ a✝) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (a✝¹.imp_ a✝))

case forall_
D : Type
I : Interpretation D
z a✝¹ : String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝ →
      Formula.lc_at j a✝ → (Holds D I V a✝ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (forall_ a✝¹ a✝)
h2 : Formula.lc_at j (forall_ a✝¹ a✝)
⊢ Holds D I V (forall_ a✝¹ a✝) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ a✝¹ a✝))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (pred_ X vs)
h2 : Formula.lc_at j (pred_ X vs)
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
Tactic:
case pred_ X vs =>
  simp only [occursIn] at h1
  simp only [Formula.lc_at] at h2
  simp only [Formula.openList]
  simp only [Holds]
  congr! 1
  simp
  simp only [List.map_eq_map_iff]
  intro v a1
  specialize h2 v a1
  simp
  cases v
  case _ x =>
    simp only [Var.openList]
    simp only [Var.close]
    have s1 : ¬ free_ x = free_ z
    intro contra
    apply h1
    simp only [← contra]
    exact a1
    simp only [if_neg s1]
  case _ i =>
    simp only [Var.lc_at] at h2
    simp only [Var.openList]
    simp
    split_ifs
    simp only [Var.close]
    simp only [if_pos h2]
Proof state after:
no goals
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi.not_
h2 : Formula.lc_at j phi.not_
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)
Tactic:
case not_ phi phi_ih =>
  simp only [occursIn] at h1
  simp only [Formula.lc_at] at h2
  simp only [Holds]
  congr! 1
  exact phi_ih V j h1 h2
Proof state after:
no goals
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (forall_ x phi)
h2 : Formula.lc_at j (forall_ x phi)
⊢ Holds D I V (forall_ x phi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ x phi))
Tactic:
case forall_ x phi phi_ih =>
  simp only [occursIn] at h1
  simp only [Formula.lc_at] at h2
  simp only [Formula.openList]
  simp only [Holds]
  apply forall_congr'
  intro d
  specialize phi_ih (shift D V d) (j + 1) h1 h2
  simp only [phi_ih]
  congr! 1
  apply extracted_1
Proof state after:
no goals
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (pred_ X vs)
h2 : Formula.lc_at j (pred_ X vs)
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
Tactic:
simp only [occursIn] at h1
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : Formula.lc_at j (pred_ X vs)
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : Formula.lc_at j (pred_ X vs)
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
Tactic:
simp only [Formula.lc_at] at h2
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
Tactic:
simp only [Formula.openList]
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (pred_ X (List.map (Var.openList j [free_ z]) vs))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (pred_ X (List.map (Var.openList j [free_ z]) vs))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ I.pred_ X (List.map V vs) ↔ I.pred_ X (List.map (V ∘ Var.close j (free_ z)) (List.map (Var.openList j [free_ z]) vs))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ I.pred_ X (List.map V vs) ↔ I.pred_ X (List.map (V ∘ Var.close j (free_ z)) (List.map (Var.openList j [free_ z]) vs))
Tactic:
congr! 1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map V vs = List.map (V ∘ Var.close j (free_ z)) (List.map (Var.openList j [free_ z]) vs)
Theorem: LN.HoldsClose
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map V vs = List.map (V ∘ Var.close j (free_ z)) (List.map (Var.openList j [free_ z]) vs)
Tactic:
simp
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map V vs = List.map ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) vs
Theorem: LN.HoldsClose
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map V vs = List.map ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) vs
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ ∀ x ∈ vs, V x = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) x
Theorem: LN.HoldsClose
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ ∀ x ∈ vs, V x = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) x
Tactic:
intro v a1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
v : Var
a1 : v ∈ vs
⊢ V v = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) v
Theorem: LN.HoldsClose
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
v : Var
a1 : v ∈ vs
⊢ V v = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) v
Tactic:
specialize h2 v a1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
v : Var
a1 : v ∈ vs
h2 : Var.lc_at j v
⊢ V v = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) v
Theorem: LN.HoldsClose
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
v : Var
a1 : v ∈ vs
h2 : Var.lc_at j v
⊢ V v = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) v
Tactic:
simp
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
v : Var
a1 : v ∈ vs
h2 : Var.lc_at j v
⊢ V v = V (Var.close j (free_ z) (Var.openList j [free_ z] v))
Theorem: LN.HoldsClose
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
v : Var
a1 : v ∈ vs
h2 : Var.lc_at j v
⊢ V v = V (Var.close j (free_ z) (Var.openList j [free_ z] v))
Tactic:
cases v
Proof state after:
case a.h.e'_4.free_
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
a✝ : String
a1 : free_ a✝ ∈ vs
h2 : Var.lc_at j (free_ a✝)
⊢ V (free_ a✝) = V (Var.close j (free_ z) (Var.openList j [free_ z] (free_ a✝)))

case a.h.e'_4.bound_
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
a✝ : ℕ
a1 : bound_ a✝ ∈ vs
h2 : Var.lc_at j (bound_ a✝)
⊢ V (bound_ a✝) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ a✝)))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (Var.close j (free_ z) (Var.openList j [free_ z] (free_ x)))
Tactic:
case _ x =>
  simp only [Var.openList]
  simp only [Var.close]
  have s1 : ¬ free_ x = free_ z
  intro contra
  apply h1
  simp only [← contra]
  exact a1
  simp only [if_neg s1]
Proof state after:
no goals
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : Var.lc_at j (bound_ i)
⊢ V (bound_ i) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ i)))
Tactic:
case _ i =>
  simp only [Var.lc_at] at h2
  simp only [Var.openList]
  simp
  split_ifs
  simp only [Var.close]
  simp only [if_pos h2]
Proof state after:
no goals
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (Var.close j (free_ z) (Var.openList j [free_ z] (free_ x)))
Tactic:
simp only [Var.openList]
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (Var.close j (free_ z) (free_ x))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (Var.close j (free_ z) (free_ x))
Tactic:
simp only [Var.close]
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
have s1 : ¬ free_ x = free_ z
Proof state after:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ ¬free_ x = free_ z

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Theorem: LN.HoldsClose
Proof state before:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ ¬free_ x = free_ z

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
intro contra
Proof state after:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ False

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Theorem: LN.HoldsClose
Proof state before:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ False

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
apply h1
Proof state after:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ free_ z ∈ vs

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Theorem: LN.HoldsClose
Proof state before:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ free_ z ∈ vs

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
simp only [← contra]
Proof state after:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ free_ x ∈ vs

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Theorem: LN.HoldsClose
Proof state before:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ free_ x ∈ vs

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
exact a1
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
simp only [if_neg s1]
Proof state after:
no goals
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : Var.lc_at j (bound_ i)
⊢ V (bound_ i) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ i)))
Tactic:
simp only [Var.lc_at] at h2
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ i)))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ i)))
Tactic:
simp only [Var.openList]
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) =
    V
      (Var.close j (free_ z)
        (if i < j then bound_ i
        else if x : i - j < [free_ z].length then [free_ z][i - j] else bound_ (i - j - [free_ z].length + j)))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) =
    V
      (Var.close j (free_ z)
        (if i < j then bound_ i
        else if x : i - j < [free_ z].length then [free_ z][i - j] else bound_ (i - j - [free_ z].length + j)))
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) =
    V (Var.close j (free_ z) (if i < j then bound_ i else if i - j = 0 then free_ z else bound_ (i - j - 1 + j)))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) =
    V (Var.close j (free_ z) (if i < j then bound_ i else if i - j = 0 then free_ z else bound_ (i - j - 1 + j)))
Tactic:
split_ifs
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (Var.close j (free_ z) (bound_ i))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (Var.close j (free_ z) (bound_ i))
Tactic:
simp only [Var.close]
Proof state after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (if i < j then bound_ i else bound_ (i + 1))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
simp only [if_pos h2]
Proof state after:
no goals
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi.not_
h2 : Formula.lc_at j phi.not_
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)
Tactic:
simp only [occursIn] at h1
Proof state after:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi.not_
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi.not_
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)
Tactic:
simp only [Formula.lc_at] at h2
Proof state after:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)