internlm/Lean-Github huggingface dataset:
Theorem: vocPreservedTwo
Proof state before:
case pos.h
X : Finset Formula
ϕ1 ϕ2 : Formula
a✝ : Char
θ : Formula
theta_in_X psi_in_X : θ ∈ X
eq_voc :
  ((match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) =
    match θ with
    | Formula.bottom => ∅
    | ·c => {c}
    | ~φ => vocabOfFormula φ
    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
    | □φ => vocabOfFormula φ
a_in_vocTheta :
  a✝ ∈
    (match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
⊢ (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
Tactic:
simp at a_in_vocTheta
Proof state after:
case pos.h
X : Finset Formula
ϕ1 ϕ2 : Formula
a✝ : Char
θ : Formula
theta_in_X psi_in_X : θ ∈ X
eq_voc :
  ((match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) =
    match θ with
    | Formula.bottom => ∅
    | ·c => {c}
    | ~φ => vocabOfFormula φ
    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
    | □φ => vocabOfFormula φ
a_in_vocTheta :
  (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
⊢ (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
Theorem: vocPreservedTwo
Proof state before:
case pos.h
X : Finset Formula
ϕ1 ϕ2 : Formula
a✝ : Char
θ : Formula
theta_in_X psi_in_X : θ ∈ X
eq_voc :
  ((match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) =
    match θ with
    | Formula.bottom => ∅
    | ·c => {c}
    | ~φ => vocabOfFormula φ
    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
    | □φ => vocabOfFormula φ
a_in_vocTheta :
  (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
⊢ (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
Tactic:
tauto
Proof state after:
no goals
Theorem: vocPreservedTwo
Proof state before:
case neg
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : ¬θ = ψ
⊢ (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Tactic:
constructor
Proof state after:
case neg.h
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : ¬θ = ψ
⊢ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
Theorem: vocPreservedTwo
Proof state before:
case neg.h
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : ¬θ = ψ
⊢ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
Tactic:
use θ
Proof state after:
no goals
Theorem: vocPreservedTwo
Proof state before:
case a.mpr.inl
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a
Tactic:
aesop
Proof state after:
no goals
Theorem: vocPreservedTwo
Proof state before:
case a.mpr.inr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a
Tactic:
use ψ
Proof state after:
case h
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ψ ∈ X ∧ a✝ ∈ vocabOfFormula ψ
Theorem: vocPreservedTwo
Proof state before:
case h
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ψ ∈ X ∧ a✝ ∈ vocabOfFormula ψ
Tactic:
constructor
Proof state after:
case h.left
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ψ ∈ X

case h.right
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ a✝ ∈ vocabOfFormula ψ
Theorem: vocPreservedTwo
Proof state before:
case h.left
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ψ ∈ X
Tactic:
aesop
Proof state after:
no goals
Theorem: vocPreservedTwo
Proof state before:
case h.right
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ a✝ ∈ vocabOfFormula ψ
Tactic:
rw [← eq_voc]
Proof state after:
case h.right
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ a✝ ∈ vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2
Theorem: vocPreservedTwo
Proof state before:
case h.right
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ a✝ ∈ vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2
Tactic:
simp
Proof state after:
case h.right
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Theorem: vocPreservedTwo
Proof state before:
case h.right
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Tactic:
aesop
Proof state after:
no goals
Theorem: vocPreservedSub
Proof state before:
X : Finset Formula
ψ ϕ : Formula
⊢ ψ ∈ X → voc ϕ ⊆ voc ψ → voc (X \ {ψ} ∪ {ϕ}) ⊆ voc X
Tactic:
intro psi_in_X sub_voc
Proof state after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : voc ϕ ⊆ voc ψ
⊢ voc (X \ {ψ} ∪ {ϕ}) ⊆ voc X
Theorem: vocPreservedSub
Proof state before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : voc ϕ ⊆ voc ψ
⊢ voc (X \ {ψ} ∪ {ϕ}) ⊆ voc X
Tactic:
simp at *
Proof state after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
⊢ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula ⊆ X.biUnion vocabOfFormula
Theorem: vocPreservedSub
Proof state before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
⊢ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula ⊆ X.biUnion vocabOfFormula
Tactic:
intro a a_in
Proof state after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
a_in : a ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
⊢ a ∈ X.biUnion vocabOfFormula
Theorem: vocPreservedSub
Proof state before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
a_in : a ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
⊢ a ∈ X.biUnion vocabOfFormula
Tactic:
norm_num at *
Proof state after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
a_in : a ∈ vocabOfFormula ϕ ∨ ∃ a_1, (¬a_1 = ψ ∧ a_1 ∈ X) ∧ a ∈ vocabOfFormula a_1
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Theorem: vocPreservedSub
Proof state before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
a_in : a ∈ vocabOfFormula ϕ ∨ ∃ a_1, (¬a_1 = ψ ∧ a_1 ∈ X) ∧ a ∈ vocabOfFormula a_1
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Tactic:
cases a_in
Proof state after:
case inl
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1

case inr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : ∃ a_1, (¬a_1 = ψ ∧ a_1 ∈ X) ∧ a ∈ vocabOfFormula a_1
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Theorem: vocPreservedSub
Proof state before:
case inl
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Tactic:
use ψ
Proof state after:
case h
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ψ ∈ X ∧ a ∈ vocabOfFormula ψ
Theorem: vocPreservedSub
Proof state before:
case h
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ψ ∈ X ∧ a ∈ vocabOfFormula ψ
Tactic:
rw [Finset.subset_iff] at sub_voc
Proof state after:
case h
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : ∀ ⦃x : Char⦄, x ∈ vocabOfFormula ϕ → x ∈ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ψ ∈ X ∧ a ∈ vocabOfFormula ψ
Theorem: vocPreservedSub
Proof state before:
case h
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : ∀ ⦃x : Char⦄, x ∈ vocabOfFormula ϕ → x ∈ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ψ ∈ X ∧ a ∈ vocabOfFormula ψ
Tactic:
tauto
Proof state after:
no goals
Theorem: vocPreservedSub
Proof state before:
case inr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : ∃ a_1, (¬a_1 = ψ ∧ a_1 ∈ X) ∧ a ∈ vocabOfFormula a_1
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Tactic:
aesop
Proof state after:
no goals
Theorem: get_eq_getzip
Proof state before:
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = (((x, X) :: δ.zip (l ++ [Y])).get ⟨↑i, h⟩).2
Tactic:
simp only [←List.zip_cons_cons]
Proof state after:
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = (((x :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i, h⟩).2
Theorem: get_eq_getzip
Proof state before:
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = (((x :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i, h⟩).2
Tactic:
rw [List.get_zip]
Proof state after:
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = ((x :: δ).get ⟨↑⟨↑i, h⟩, ⋯⟩, (X :: (l ++ [Y])).get ⟨↑⟨↑i, h⟩, ⋯⟩).2
Theorem: get_eq_getzip
Proof state before:
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = ((x :: δ).get ⟨↑⟨↑i, h⟩, ⋯⟩, (X :: (l ++ [Y])).get ⟨↑⟨↑i, h⟩, ⋯⟩).2
Tactic:
rfl
Proof state after:
no goals
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
i : Fin (X :: l ++ [Y]).length
⊢ (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
Tactic:
induction i using Fin.inductionOn
Proof state after:
case zero
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
⊢ (⌈⌈List.drop (↑0) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get 0)

case succ
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
i✝ : Fin (l.append [Y]).length
a✝ : (⌈⌈List.drop (↑i✝.castSucc) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i✝.castSucc)
⊢ (⌈⌈List.drop (↑i✝.succ) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i✝.succ)
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
⊢ (⌈⌈List.drop (↑0) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get 0)
Tactic:
case zero =>
  simp_all only [instBot, insTop, List.cons_append, List.zip_cons_cons, Subtype.forall,
    List.length_cons, Nat.succ_eq_add_one, Fin.val_zero, List.drop_zero, List.get_cons_zero]
Proof state after:
no goals
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
⊢ (⌈⌈List.drop (↑0) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get 0)
Tactic:
simp_all only [instBot, insTop, List.cons_append, List.zip_cons_cons, Subtype.forall,
  List.length_cons, Nat.succ_eq_add_one, Fin.val_zero, List.drop_zero, List.get_cons_zero]
Proof state after:
no goals
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
i : Fin (l.append [Y]).length
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)
⊢ (⌈⌈List.drop (↑i.succ) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.succ)
Tactic:
simp_all only [List.cons_append, List.length_cons, List.append_eq, Fin.val_succ, List.get_cons_succ']
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
⊢ (⌈⌈List.drop (↑i + 1) δ⌉⌉φ) ∈ ↑((l ++ [Y]).get i)
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
⊢ (⌈⌈List.drop (↑i + 1) δ⌉⌉φ) ∈ ↑((l ++ [Y]).get i)
Tactic:
have help1 : (List.append l [Y]).length = δ.length := by simp [length_def]
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ (⌈⌈List.drop (↑i + 1) δ⌉⌉φ) ∈ ↑((l ++ [Y]).get i)
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ (⌈⌈List.drop (↑i + 1) δ⌉⌉φ) ∈ ↑((l ++ [Y]).get i)
Tactic:
apply IHδ (δ.get (i.cast help1)) (by apply List.get_mem) (List.get (X :: l ++ [Y]) i.castSucc)
Proof state after:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)

case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: l ++ [Y]).get i.castSucc) ((l ++ [Y]).get i)
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
⊢ (l.append [Y]).length = δ.length
Tactic:
simp [length_def]
Proof state after:
no goals
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ δ.get (Fin.cast help1 i) ∈ δ
Tactic:
apply List.get_mem
Proof state after:
no goals