internlm/Lean-Github huggingface dataset:
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
⊢ 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 [Holds]
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 ↔ ¬Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
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
⊢ ¬Holds D I V phi ↔ ¬Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
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 ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
Theorem: LN.HoldsClose
Proof state before:
case a.h.e'_1.a
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 ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
Tactic:
exact phi_ih V j h1 h2
Proof state after:
no goals
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (phi.imp_ psi)
h2 : Formula.lc_at j (phi.imp_ psi)
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
simp only [occursIn] at h1
Proof state after:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1 : ¬(occursIn (free_ z) phi ∨ occursIn (free_ z) psi)
h2 : Formula.lc_at j (phi.imp_ psi)
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1 : ¬(occursIn (free_ z) phi ∨ occursIn (free_ z) psi)
h2 : Formula.lc_at j (phi.imp_ psi)
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
push_neg at h1
Proof state after:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j (phi.imp_ psi)
h1 : ¬occursIn (free_ z) phi ∧ ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j (phi.imp_ psi)
h1 : ¬occursIn (free_ z) phi ∧ ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
simp only [Formula.lc_at] at h2
Proof state after:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j phi ∧ Formula.lc_at j psi
h1 : ¬occursIn (free_ z) phi ∧ ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j phi ∧ Formula.lc_at j psi
h1 : ¬occursIn (free_ z) phi ∧ ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
cases h1
Proof state after:
case intro
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j phi ∧ Formula.lc_at j psi
left✝ : ¬occursIn (free_ z) phi
right✝ : ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j phi ∧ Formula.lc_at j psi
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
cases h2
Proof state after:
case intro
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
left✝ : Formula.lc_at j phi
right✝ : Formula.lc_at j psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
⊢ Holds D I V phi → Holds D I V psi ↔
    Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi) →
      Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi)
Theorem: LN.HoldsClose
Proof state before:
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
⊢ Holds D I V phi → Holds D I V psi ↔
    Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi) →
      Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi)
Tactic:
congr! 1
Proof state after:
case a.h.a
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
⊢ Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)

case a.h'.a
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
a✝ : Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
⊢ Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi)
Theorem: LN.HoldsClose
Proof state before:
case a.h.a
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
⊢ Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
Tactic:
exact phi_ih V j h1_left h2_left
Proof state after:
no goals
Theorem: LN.HoldsClose
Proof state before:
case a.h'.a
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
a✝ : Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
⊢ Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi)
Tactic:
exact psi_ih V j h1_right h2_right
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:
simp only [occursIn] at h1
Proof state after:
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) 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))
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) 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:
simp only [Formula.lc_at] at h2
Proof state after:
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) phi
h2 : Formula.lc_at (j + 1) 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))
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) phi
h2 : Formula.lc_at (j + 1) 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:
simp only [Formula.openList]
Proof state after:
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) phi
h2 : Formula.lc_at (j + 1) phi
⊢ Holds D I V (forall_ x phi) ↔
    Holds D I (V ∘ Var.close j (free_ z)) (forall_ x (Formula.openList (j + 1) [free_ z] phi))
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) phi
h2 : Formula.lc_at (j + 1) phi
⊢ Holds D I V (forall_ x phi) ↔
    Holds D I (V ∘ Var.close j (free_ z)) (forall_ x (Formula.openList (j + 1) [free_ z] phi))
Tactic:
simp only [Holds]
Proof state after:
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) phi
h2 : Formula.lc_at (j + 1) phi
⊢ (∀ (d : D), Holds D I (shift D V d) phi) ↔
    ∀ (d : D), Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
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) phi
h2 : Formula.lc_at (j + 1) phi
⊢ (∀ (d : D), Holds D I (shift D V d) phi) ↔
    ∀ (d : D), Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
Tactic:
apply forall_congr'
Proof state after:
case h
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) phi
h2 : Formula.lc_at (j + 1) phi
⊢ ∀ (a : D),
    Holds D I (shift D V a) phi ↔
      Holds D I (shift D (V ∘ Var.close j (free_ z)) a) (Formula.openList (j + 1) [free_ z] phi)
Theorem: LN.HoldsClose
Proof state before:
case h
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) phi
h2 : Formula.lc_at (j + 1) phi
⊢ ∀ (a : D),
    Holds D I (shift D V a) phi ↔
      Holds D I (shift D (V ∘ Var.close j (free_ z)) a) (Formula.openList (j + 1) [free_ z] phi)
Tactic:
intro d
Proof state after:
case h
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) phi
h2 : Formula.lc_at (j + 1) phi
d : D
⊢ Holds D I (shift D V d) phi ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
Theorem: LN.HoldsClose
Proof state before:
case h
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) phi
h2 : Formula.lc_at (j + 1) phi
d : D
⊢ Holds D I (shift D V d) phi ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
Tactic:
specialize phi_ih (shift D V d) (j + 1) h1 h2
Proof state after:
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) phi ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
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) phi ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
Tactic:
simp only [phi_ih]
Proof state after:
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)