internlm/Lean-Github huggingface dataset:
Theorem: loadClaimHelper
Proof state before:
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 :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
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
⊢ ↑i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1
Tactic:
rcases i with ⟨val, hyp⟩
Proof state after:
case a.mk
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 :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
val : ℕ
hyp : val < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val, hyp⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, hyp⟩.castSucc)
⊢ ↑⟨val, hyp⟩ < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1
Theorem: loadClaimHelper
Proof state before:
case a.mk
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 :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
val : ℕ
hyp : val < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val, hyp⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, hyp⟩.castSucc)
⊢ ↑⟨val, hyp⟩ < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1
Tactic:
simp_all only [insTop, List.zip_cons_cons, List.length_cons, List.length_zip,
  List.length_append, List.length_singleton, min_self, Nat.succ_eq_add_one,
  add_tsub_cancel_right, instBot, List.get_cons_succ, List.get_zip, Subtype.forall,
  List.append_eq, Fin.castSucc_mk]
Proof state after:
case a.mk
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
val : ℕ
hyp : val < (l.append [Y]).length
lchain : ∀ i < δ.length, True
IHδ :
  ∀ d ∈ δ,
    ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds) (φ' : Formula),
      (⌈d⌉φ') ∈ a → relate (↑MG) d ⟨a, b⟩ ⟨a_1, b_1⟩ → φ' ∈ a_1
help1 : l.length + ([].length + 1) = δ.length
IH : (⌈⌈List.drop val δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, ⋯⟩)
⊢ val < δ.length
Theorem: loadClaimHelper
Proof state before:
case a.mk
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
val : ℕ
hyp : val < (l.append [Y]).length
lchain : ∀ i < δ.length, True
IHδ :
  ∀ d ∈ δ,
    ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds) (φ' : Formula),
      (⌈d⌉φ') ∈ a → relate (↑MG) d ⟨a, b⟩ ⟨a_1, b_1⟩ → φ' ∈ a_1
help1 : l.length + ([].length + 1) = δ.length
IH : (⌈⌈List.drop val δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, ⋯⟩)
⊢ val < δ.length
Tactic:
rw [← length_def]
Proof state after:
case a.mk
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
val : ℕ
hyp : val < (l.append [Y]).length
lchain : ∀ i < δ.length, True
IHδ :
  ∀ d ∈ δ,
    ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds) (φ' : Formula),
      (⌈d⌉φ') ∈ a → relate (↑MG) d ⟨a, b⟩ ⟨a_1, b_1⟩ → φ' ∈ a_1
help1 : l.length + ([].length + 1) = δ.length
IH : (⌈⌈List.drop val δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, ⋯⟩)
⊢ val < l.length + 1
Theorem: loadClaimHelper
Proof state before:
case a.mk
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
val : ℕ
hyp : val < (l.append [Y]).length
lchain : ∀ i < δ.length, True
IHδ :
  ∀ d ∈ δ,
    ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds) (φ' : Formula),
      (⌈d⌉φ') ∈ a → relate (↑MG) d ⟨a, b⟩ ⟨a_1, b_1⟩ → φ' ∈ a_1
help1 : l.length + ([].length + 1) = δ.length
IH : (⌈⌈List.drop val δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, ⋯⟩)
⊢ val < l.length + 1
Tactic:
simp at hyp
Proof state after:
case a.mk
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
val : ℕ
hyp✝ : val < (l.append [Y]).length
lchain : ∀ i < δ.length, True
IHδ :
  ∀ d ∈ δ,
    ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds) (φ' : Formula),
      (⌈d⌉φ') ∈ a → relate (↑MG) d ⟨a, b⟩ ⟨a_1, b_1⟩ → φ' ∈ a_1
help1 : l.length + ([].length + 1) = δ.length
IH : (⌈⌈List.drop val δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, ⋯⟩)
hyp : val < l.length + 1
⊢ val < l.length + 1
Theorem: loadClaimHelper
Proof state before:
case a.mk
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
val : ℕ
hyp✝ : val < (l.append [Y]).length
lchain : ∀ i < δ.length, True
IHδ :
  ∀ d ∈ δ,
    ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds) (φ' : Formula),
      (⌈d⌉φ') ∈ a → relate (↑MG) d ⟨a, b⟩ ⟨a_1, b_1⟩ → φ' ∈ a_1
help1 : l.length + ([].length + 1) = δ.length
IH : (⌈⌈List.drop val δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, ⋯⟩)
hyp : val < l.length + 1
⊢ val < l.length + 1
Tactic:
exact hyp
Proof state after:
no goals
Theorem: loadClaimHelper
Proof state before:
case h.e'_3.h.e'_3.h.e'_2.h.e'_1
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
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
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
⊢ δ.length = (l ++ [Y]).length
Tactic:
rw [← length_def]
Proof state after:
case h.e'_3.h.e'_3.h.e'_2.h.e'_1
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
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
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
⊢ l.length + 1 = (l ++ [Y]).length
Theorem: loadClaimHelper
Proof state before:
case h.e'_3.h.e'_3.h.e'_2.h.e'_1
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
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
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
⊢ l.length + 1 = (l ++ [Y]).length
Tactic:
simp only [List.length_append, List.length_singleton]
Proof state after:
no goals
Theorem: loadClaimHelper
Proof state before:
case h.e'_3.h.e'_3.h.e'_2.h.e'_2
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
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
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
e_1✝ : δ.length = (l ++ [Y]).length
⊢ HEq (Fin.cast help1 i) i
Tactic:
simp only [Fin.cast, List.append_eq]
Proof state after:
case h.e'_3.h.e'_3.h.e'_2.h.e'_2
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
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
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
e_1✝ : δ.length = (l ++ [Y]).length
⊢ HEq ⟨↑i, ⋯⟩ i
Theorem: loadClaimHelper
Proof state before:
case h.e'_3.h.e'_3.h.e'_2.h.e'_2
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
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
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
e_1✝ : δ.length = (l ++ [Y]).length
⊢ HEq ⟨↑i, ⋯⟩ i
Tactic:
rcases i with ⟨val, hyp⟩
Proof state after:
case h.e'_3.h.e'_3.h.e'_2.h.e'_2.mk
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
e_1✝ : δ.length = (l ++ [Y]).length
val : ℕ
hyp : val < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val, hyp⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, hyp⟩.castSucc)
lchain :
  relate (↑MG) (δ.get ⟨↑⟨val, hyp⟩, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑⟨val, hyp⟩, ⋯⟩).2
    ((l ++ [Y]).get ⟨↑⟨val, hyp⟩, ⋯⟩)
⊢ HEq ⟨↑⟨val, hyp⟩, ⋯⟩ ⟨val, hyp⟩
Theorem: loadClaimHelper
Proof state before:
case h.e'_3.h.e'_3.h.e'_2.h.e'_2.mk
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
e_1✝ : δ.length = (l ++ [Y]).length
val : ℕ
hyp : val < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val, hyp⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, hyp⟩.castSucc)
lchain :
  relate (↑MG) (δ.get ⟨↑⟨val, hyp⟩, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑⟨val, hyp⟩, ⋯⟩).2
    ((l ++ [Y]).get ⟨↑⟨val, hyp⟩, ⋯⟩)
⊢ HEq ⟨↑⟨val, hyp⟩, ⋯⟩ ⟨val, hyp⟩
Tactic:
rw [Fin.heq_ext_iff]
Proof state after:
case h.e'_3.h.e'_3.h.e'_2.h.e'_2.mk.h
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
e_1✝ : δ.length = (l ++ [Y]).length
val : ℕ
hyp : val < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val, hyp⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, hyp⟩.castSucc)
lchain :
  relate (↑MG) (δ.get ⟨↑⟨val, hyp⟩, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑⟨val, hyp⟩, ⋯⟩).2
    ((l ++ [Y]).get ⟨↑⟨val, hyp⟩, ⋯⟩)
⊢ δ.length = (l.append [Y]).length
Theorem: loadClaimHelper
Proof state before:
case h.e'_3.h.e'_3.h.e'_2.h.e'_2.mk.h
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
e_1✝ : δ.length = (l ++ [Y]).length
val : ℕ
hyp : val < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val, hyp⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, hyp⟩.castSucc)
lchain :
  relate (↑MG) (δ.get ⟨↑⟨val, hyp⟩, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑⟨val, hyp⟩, ⋯⟩).2
    ((l ++ [Y]).get ⟨↑⟨val, hyp⟩, ⋯⟩)
⊢ δ.length = (l.append [Y]).length
Tactic:
rw [← length_def]
Proof state after:
case h.e'_3.h.e'_3.h.e'_2.h.e'_2.mk.h
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
e_1✝ : δ.length = (l ++ [Y]).length
val : ℕ
hyp : val < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val, hyp⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, hyp⟩.castSucc)
lchain :
  relate (↑MG) (δ.get ⟨↑⟨val, hyp⟩, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑⟨val, hyp⟩, ⋯⟩).2
    ((l ++ [Y]).get ⟨↑⟨val, hyp⟩, ⋯⟩)
⊢ l.length + 1 = (l.append [Y]).length
Theorem: loadClaimHelper
Proof state before:
case h.e'_3.h.e'_3.h.e'_2.h.e'_2.mk.h
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
e_1✝ : δ.length = (l ++ [Y]).length
val : ℕ
hyp : val < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val, hyp⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, hyp⟩.castSucc)
lchain :
  relate (↑MG) (δ.get ⟨↑⟨val, hyp⟩, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑⟨val, hyp⟩, ⋯⟩).2
    ((l ++ [Y]).get ⟨↑⟨val, hyp⟩, ⋯⟩)
⊢ l.length + 1 = (l.append [Y]).length
Tactic:
simp only [List.append_eq, List.length_append, List.length_singleton]
Proof state after:
no goals
Theorem: loadClaimHelper
Proof state before:
case h.e'_4
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✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
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
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
⊢ (X :: (l ++ [Y])).get i.castSucc = (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2
Tactic:
apply get_eq_getzip
Proof state after:
no goals
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X Y : { x // x ∈ Worlds }
⊢ Q (↑MG).Rel α X Y → relate (↑MG) α X Y
Tactic:
cases α
Proof state after:
case atom_prog
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : ℕ
⊢ Q (↑MG).Rel (·a✝) X Y → relate (↑MG) (·a✝) X Y

case sequence
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝¹ a✝ : Program
⊢ Q (↑MG).Rel (a✝¹;'a✝) X Y → relate (↑MG) (a✝¹;'a✝) X Y

case union
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝¹ a✝ : Program
⊢ Q (↑MG).Rel (a✝¹⋓a✝) X Y → relate (↑MG) (a✝¹⋓a✝) X Y

case star
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : Program
⊢ Q (↑MG).Rel (∗a✝) X Y → relate (↑MG) (∗a✝) X Y

case test
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : Formula
⊢ Q (↑MG).Rel (?'a✝) X Y → relate (↑MG) (?'a✝) X Y
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : ℕ
⊢ Q (↑MG).Rel (·a✝) X Y → relate (↑MG) (·a✝) X Y
Tactic:
case atom_prog =>
  simp only [instBot, Q, relate, imp_self]
Proof state after:
no goals
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Tactic:
case sequence α β =>
  have := Q_then_relate MG α
  have := Q_then_relate MG β
  simp only [instBot, Subtype.forall, Q, Relation.Comp, Subtype.exists,
    relate, forall_exists_index, and_imp] at *
  tauto
Proof state after:
no goals
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Tactic:
case union α β =>
  have := Q_then_relate MG α
  have := Q_then_relate MG β
  simp only [instBot, Subtype.forall, Q, relate] at *
  tauto
Proof state after:
no goals
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ Q (↑MG).Rel (∗α) X Y → relate (↑MG) (∗α) X Y
Tactic:
case star α =>
  simp only [instBot, Q, relate]
  apply Relation.ReflTransGen.lift
  intro a b Qab
  exact Q_then_relate MG α a b Qab
Proof state after:
no goals
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : ℕ
⊢ Q (↑MG).Rel (·a✝) X Y → relate (↑MG) (·a✝) X Y
Tactic:
simp only [instBot, Q, relate, imp_self]
Proof state after:
no goals
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Tactic:
have := Q_then_relate MG α
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Tactic:
have := Q_then_relate MG β
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel β X Y → relate (↑MG) β X Y
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel β X Y → relate (↑MG) β X Y
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Tactic:
simp only [instBot, Subtype.forall, Q, Relation.Comp, Subtype.exists,
  relate, forall_exists_index, and_imp] at *
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel α ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) α ⟨a, b⟩ ⟨a_1, b_1⟩
this :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel β ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) β ⟨a, b⟩ ⟨a_1, b_1⟩
⊢ ∀ (x : Finset Formula) (x_1 : x ∈ Worlds),
    Q (↑MG).Rel α X ⟨x, x_1⟩ →
      Q (↑MG).Rel β ⟨x, x_1⟩ Y → ∃ a, ∃ (b : a ∈ Worlds), relate (↑MG) α X ⟨a, b⟩ ∧ relate (↑MG) β ⟨a, b⟩ Y