internlm/Lean-Github huggingface dataset:
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
_forTermination : lengthOfFormula ψ < lengthOfProgram (∗β)
⊢ ψ ∈ ↑X
Tactic:
apply mysat
Proof state after:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
_forTermination : lengthOfFormula ψ < lengthOfProgram (∗β)
⊢ ψ ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = ψ
Theorem: loadedTruthLemmaProg
Proof state before:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
_forTermination : lengthOfFormula ψ < lengthOfProgram (∗β)
⊢ ψ ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = ψ
Tactic:
left
Proof state after:
case a.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
_forTermination : lengthOfFormula ψ < lengthOfProgram (∗β)
⊢ ψ ∈ F (∗β) ℓ
Theorem: loadedTruthLemmaProg
Proof state before:
case a.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
_forTermination : lengthOfFormula ψ < lengthOfProgram (∗β)
⊢ ψ ∈ F (∗β) ℓ
Tactic:
simp [F]
Proof state after:
case a.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
_forTermination : lengthOfFormula ψ < lengthOfProgram (∗β)
⊢ ψ ∈ F β fun x => ℓ ⟨↑x, ⋯⟩
Theorem: loadedTruthLemmaProg
Proof state before:
case a.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
_forTermination : lengthOfFormula ψ < lengthOfProgram (∗β)
⊢ ψ ∈ F β fun x => ℓ ⟨↑x, ⋯⟩
Tactic:
assumption
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
⊢ lengthOfFormula ψ < lengthOfProgram (∗β)
Tactic:
apply F_goes_down
Proof state after:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
⊢ ψ ∈ F (∗β) ?ℓ

case ℓ
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
⊢ TP (∗β)
Theorem: loadedTruthLemmaProg
Proof state before:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
⊢ ψ ∈ F β fun x => ?ℓ ⟨↑x, ⋯⟩

case ℓ
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
⊢ TP (∗β)
Tactic:
convert ψ_in
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in_P :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ X Z
hyp : δ = []
⊢ φ ∈ ↑Y
Tactic:
subst hyp
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : relateSeq ↑MG [] X Z
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : relateSeq ↑MG [] X Z
⊢ φ ∈ ↑Y
Tactic:
simp only [relateSeq] at X_δ_Z
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ φ ∈ ↑Y
Tactic:
apply innerIH X φ boxP_in_X
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ ∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_1
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ X = YS.tail.head
Tactic:
rw [← Vector.get_zero]
Proof state after:
case refine_1
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ X = YS.tail.get 0
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_1
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ X = YS.tail.get 0
Tactic:
rw [Vector.get_tail_succ]
Proof state after:
case refine_1
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ X = YS.get (Fin.succ 0)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_1
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ X = YS.get (Fin.succ 0)
Tactic:
aesop
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_2
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ Y = YS.tail.last
Tactic:
rw [Vector.last_def]
Proof state after:
case refine_2
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ Y = YS.tail.get (Fin.last m)