Theorem: loadClaimHelper (Pdl/Modelgraphs.lean)

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
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)

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]
State after:
no goals

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]
State after:
no goals

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']
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)

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]
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)

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)
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)

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]
State after:
no goals

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
State after:
no goals

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 : 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)
Tactic:
have : (⌈List.get δ (i.cast help1)⌉⌈⌈List.drop (i + 1) δ⌉⌉φ) = (⌈⌈List.drop (i.castSucc) δ⌉⌉φ) := by
  simp only [List.append_eq, Fin.coe_castSucc]
  rw [← Formula.boxes]
  have := @List.drop_eq_get_cons _ i δ (by rw [← length_def]; have := Fin.is_lt i; convert this; simp)
  rw [this]
  cases i
  simp_all only [instBot, insTop, List.zip_cons_cons, Subtype.forall, List.append_eq,
    Fin.castSucc_mk, boxes, Fin.cast_mk]
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
this : (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ
⊢ (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)

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 : 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
this : (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ
⊢ (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)
Tactic:
rw [this]
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
this : (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ
⊢ (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)

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 : 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
this : (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ
⊢ (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)
Tactic:
exact IH
State after:
no goals

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)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ
Tactic:
simp only [List.append_eq, Fin.coe_castSucc]
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
⊢ (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ

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)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ
Tactic:
rw [← Formula.boxes]
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
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ

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) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ
Tactic:
have := @List.drop_eq_get_cons _ i δ (by rw [← length_def]; have := Fin.is_lt i; convert this; simp)
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
this : List.drop (↑i) δ = δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ

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
this : List.drop (↑i) δ = δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ
Tactic:
rw [this]
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
this : List.drop (↑i) δ = δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ⌉⌉φ

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
this : List.drop (↑i) δ = δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ⌉⌉φ
Tactic:
cases i
State after:
case 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 : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
val✝ : ℕ
isLt✝ : val✝ < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val✝, isLt✝⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val✝, isLt✝⟩.castSucc)
this : List.drop (↑⟨val✝, isLt✝⟩) δ = δ.get ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 ⟨val✝, isLt✝⟩) :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ⌉⌉φ) =
    ⌈⌈δ.get ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ⌉⌉φ

State before:
case 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 : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
val✝ : ℕ
isLt✝ : val✝ < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val✝, isLt✝⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val✝, isLt✝⟩.castSucc)
this : List.drop (↑⟨val✝, isLt✝⟩) δ = δ.get ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 ⟨val✝, isLt✝⟩) :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ⌉⌉φ) =
    ⌈⌈δ.get ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ⌉⌉φ
Tactic:
simp_all only [instBot, insTop, List.zip_cons_cons, Subtype.forall, List.append_eq,
  Fin.castSucc_mk, boxes, Fin.cast_mk]
State after:
no goals

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
⊢ ↑i < δ.length
Tactic:
rw [← length_def]
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
⊢ ↑i < l.length + 1

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
⊢ ↑i < l.length + 1
Tactic:
have := Fin.is_lt i
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
this : ↑i < (l.append [Y]).length
⊢ ↑i < l.length + 1

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
this : ↑i < (l.append [Y]).length
⊢ ↑i < l.length + 1
Tactic:
convert this
State after:
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 : 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
this : ↑i < (l.append [Y]).length
⊢ l.length + 1 = (l.append [Y]).length

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 : 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
this : ↑i < (l.append [Y]).length
⊢ l.length + 1 = (l.append [Y]).length
Tactic:
simp
State after:
no goals

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 : 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)
Tactic:
simp [relate]
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
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)

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 : 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)
Tactic:
rw [List.chain'_iff_get] at lchain
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 :
  ∀ (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
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)

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
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)
Tactic:
specialize lchain i ?_
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 :
  ∀ (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

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
lchain :
  pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i, ⋯⟩)
    ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i + 1, ⋯⟩)
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)

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
lchain :
  pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i, ⋯⟩)
    ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i + 1, ⋯⟩)
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)
Tactic:
simp only [pairRel, instBot, insTop, List.cons_append, List.zip_cons_cons, List.length_cons, List.append_eq, List.get_cons_succ, List.get_zip] at lchain
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✝ :
  ∀ (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, ⋯⟩)
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)

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
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)
Tactic:
convert lchain
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, ⋯⟩)
⊢ δ.length = (l ++ [Y]).length

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

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

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⟩
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

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]
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

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]
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

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
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

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
State after:
no goals

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]
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

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]
State after:
no goals

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]
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

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⟩
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⟩

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]
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

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]
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

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]
State after:
no goals

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
State after:
no goals