internlm/Lean-Github huggingface dataset:
Theorem: LN.ShiftVarOpenList
Proof state before:
case h
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
v : Var
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d v = (shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)) v
Tactic:
simp
Proof state after:
case h
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
v : Var
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d v = shift D V d (Var.openList (j + 1) (List.map free_ zs) v)
Theorem: LN.ShiftVarOpenList
Proof state before:
case h
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
v : Var
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d v = shift D V d (Var.openList (j + 1) (List.map free_ zs) v)
Tactic:
cases v
Proof state after:
case h.free_
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
a✝ : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ a✝) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (free_ a✝))

case h.bound_
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
a✝ : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ a✝) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ a✝))
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ x) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (free_ x))
Tactic:
case _ x =>
  simp only [Var.openList]
  simp only [shift]
  simp
Proof state after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ V (Var.openList j (List.map free_ zs) (free_ x)) = V (free_ x)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ i) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ i))
Tactic:
case _ i =>
  cases i
  case zero =>
    simp only [shift]
    simp only [Var.openList]
    simp
  case succ i =>
      simp only [shift]
      simp only [Var.openList]
      simp
      split
      case _ c1 =>
        have s1 : i + 1 < j + 1
        linarith
        simp only [if_pos s1]
      case _ c1 =>
        have s1 : ¬ i + 1 < j + 1
        linarith
        simp only [if_neg s1]
        split
        case _ c2 =>
          simp
        case _ c2 =>
          simp
Proof state after:
no goals
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ x) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (free_ x))
Tactic:
simp only [Var.openList]
Proof state after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ x) = shift D V d (free_ x)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ x) = shift D V d (free_ x)
Tactic:
simp only [shift]
Proof state after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ (V ∘ Var.openList j (List.map free_ zs)) (free_ x) = V (free_ x)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ (V ∘ Var.openList j (List.map free_ zs)) (free_ x) = V (free_ x)
Tactic:
simp
Proof state after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ V (Var.openList j (List.map free_ zs) (free_ x)) = V (free_ x)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ i) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ i))
Tactic:
cases i
Proof state after:
case zero
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ 0) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ 0))

case succ
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
n✝ : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ (n✝ + 1)) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ (n✝ + 1)))
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ 0) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ 0))
Tactic:
case zero =>
  simp only [shift]
  simp only [Var.openList]
  simp
Proof state after:
no goals
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ (i + 1)) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ (i + 1)))
Tactic:
case succ i =>
    simp only [shift]
    simp only [Var.openList]
    simp
    split
    case _ c1 =>
      have s1 : i + 1 < j + 1
      linarith
      simp only [if_pos s1]
    case _ c1 =>
      have s1 : ¬ i + 1 < j + 1
      linarith
      simp only [if_neg s1]
      split
      case _ c2 =>
        simp
      case _ c2 =>
        simp
Proof state after:
case h_3
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
i✝ : ℕ
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ i✝.succ
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (bound_ i✝)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ 0) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ 0))
Tactic:
simp only [shift]
Proof state after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ d =
    match Var.openList (j + 1) (List.map free_ zs) (bound_ 0) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ d =
    match Var.openList (j + 1) (List.map free_ zs) (bound_ 0) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Tactic:
simp only [Var.openList]
Proof state after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ d =
    match
      if 0 < j + 1 then bound_ 0
      else
        if x : 0 - (j + 1) < (List.map free_ zs).length then (List.map free_ zs)[0 - (j + 1)]
        else bound_ (0 - (j + 1) - (List.map free_ zs).length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ d =
    match
      if 0 < j + 1 then bound_ 0
      else
        if x : 0 - (j + 1) < (List.map free_ zs).length then (List.map free_ zs)[0 - (j + 1)]
        else bound_ (0 - (j + 1) - (List.map free_ zs).length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Tactic:
simp
Proof state after:
no goals
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ (i + 1)) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ (i + 1)))
Tactic:
simp only [shift]
Proof state after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ (V ∘ Var.openList j (List.map free_ zs)) (bound_ i) =
    match Var.openList (j + 1) (List.map free_ zs) (bound_ (i + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ (V ∘ Var.openList j (List.map free_ zs)) (bound_ i) =
    match Var.openList (j + 1) (List.map free_ zs) (bound_ (i + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Tactic:
simp only [Var.openList]
Proof state after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ (V ∘ Var.openList j (List.map free_ zs)) (bound_ i) =
    match
      if i + 1 < j + 1 then bound_ (i + 1)
      else
        if x : i + 1 - (j + 1) < (List.map free_ zs).length then (List.map free_ zs)[i + 1 - (j + 1)]
        else bound_ (i + 1 - (j + 1) - (List.map free_ zs).length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ (V ∘ Var.openList j (List.map free_ zs)) (bound_ i) =
    match
      if i + 1 < j + 1 then bound_ (i + 1)
      else
        if x : i + 1 - (j + 1) < (List.map free_ zs).length then (List.map free_ zs)[i + 1 - (j + 1)]
        else bound_ (i + 1 - (j + 1) - (List.map free_ zs).length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Tactic:
simp
Proof state after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) =
    match
      if i < j then bound_ (i + 1)
      else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) =
    match
      if i < j then bound_ (i + 1)
      else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Tactic:
split
Proof state after:
case h_1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)

case h_2
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d

case h_3
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
i✝ : ℕ
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ i✝.succ
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (bound_ i✝)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)
Tactic:
case _ c1 =>
  have s1 : i + 1 < j + 1
  linarith
  simp only [if_pos s1]
Proof state after:
case s1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ i + 1 < j + 1

D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
s1 : i + 1 < j + 1
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d
Tactic:
case _ c1 =>
  have s1 : ¬ i + 1 < j + 1
  linarith
  simp only [if_neg s1]
  split
  case _ c2 =>
    simp
  case _ c2 =>
    simp
Proof state after:
case s1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ ¬i + 1 < j + 1

D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
s1 : ¬i + 1 < j + 1
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)
Tactic:
have s1 : i + 1 < j + 1
Proof state after:
case s1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ i + 1 < j + 1

D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
s1 : i + 1 < j + 1
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d
Tactic:
have s1 : ¬ i + 1 < j + 1
Proof state after:
case s1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ ¬i + 1 < j + 1

D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
s1 : ¬i + 1 < j + 1
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
j : ℕ
zs : List String
F : Formula
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) F ↔ Holds D I V (Formula.openList j (List.map free_ zs) F)
Tactic:
induction F generalizing V j
Proof state after:
case pred_
D : Type
I : Interpretation D
zs : List String
a✝¹ : String
a✝ : List Var
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (pred_ a✝¹ a✝) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (pred_ a✝¹ a✝))

case not_
D : Type
I : Interpretation D
zs : List String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝.not_ ↔
    Holds D I V (Formula.openList j (List.map free_ zs) a✝.not_)

case imp_
D : Type
I : Interpretation D
zs : List String
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝¹ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (a✝¹.imp_ a✝) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (a✝¹.imp_ a✝))

case forall_
D : Type
I : Interpretation D
zs : List String
a✝¹ : String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (forall_ a✝¹ a✝) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (forall_ a✝¹ a✝))
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (pred_ X vs) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (pred_ X vs))
Tactic:
case pred_ X vs =>
  simp only [Holds]
  congr! 1
  simp
Proof state after:
no goals
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi.not_ ↔
    Holds D I V (Formula.openList j (List.map free_ zs) phi.not_)
Tactic:
case not_ phi phi_ih =>
  simp only [Holds]
  congr! 1
  apply phi_ih
Proof state after:
no goals
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (forall_ a✝ phi) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (forall_ a✝ phi))
Tactic:
case forall_ _ phi phi_ih =>
  simp only [Holds]
  apply forall_congr'
  intro d
  simp only [← phi_ih]
  congr!
  apply ShiftVarOpenList
Proof state after:
no goals
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (pred_ X vs) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (pred_ X vs))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ I.pred_ X (List.map (V ∘ Var.openList j (List.map free_ zs)) vs) ↔
    I.pred_ X (List.map V (List.map (Var.openList j (List.map free_ zs)) vs))
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ I.pred_ X (List.map (V ∘ Var.openList j (List.map free_ zs)) vs) ↔
    I.pred_ X (List.map V (List.map (Var.openList j (List.map free_ zs)) vs))
Tactic:
congr! 1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ List.map (V ∘ Var.openList j (List.map free_ zs)) vs = List.map V (List.map (Var.openList j (List.map free_ zs)) vs)
Theorem: LN.HoldsOpenList
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ List.map (V ∘ Var.openList j (List.map free_ zs)) vs = List.map V (List.map (Var.openList j (List.map free_ zs)) vs)
Tactic:
simp
Proof state after:
no goals
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi.not_ ↔
    Holds D I V (Formula.openList j (List.map free_ zs) phi.not_)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ ¬Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ ¬Holds D I V (Formula.openList j (List.map free_ zs) phi)
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ ¬Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ ¬Holds D I V (Formula.openList j (List.map free_ zs) phi)
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
Theorem: LN.HoldsOpenList
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
Tactic:
apply phi_ih
Proof state after:
no goals
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (phi.imp_ psi) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (phi.imp_ psi))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi → Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔
    Holds D I V (Formula.openList j (List.map free_ zs) phi) → Holds D I V (Formula.openList j (List.map free_ zs) psi)