Theorem: loadedTruthLemmaProg (Pdl/Modelgraphs.lean)

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
⊢ φ ∈ ↑Y
Tactic:
case inr δ_notEmpty =>
  have := relateSeq_toChain' X_δ_Y δ_notEmpty
  rcases this with ⟨l, length_def, lchain⟩
  suffices loadClaim : ∀ i : Fin (X :: l ++ [Y]).length,
      (⌈⌈δ.drop i⌉⌉φ) ∈ ((X :: l ++ [Y]).get i).val by
    specialize loadClaim (Fin.last _)
    simp [length_def] at loadClaim
    convert loadClaim
    have := @List.get_last _ Y (X :: l) (Fin.last _)
    simp_all [eq_comm]
  intro i
  exact loadClaimHelper length_def δφ_in_X lchain IHδ i
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
⊢ ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
Tactic:
intro τ τ_in
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ : Formula
τ_in : τ ∈ F (?'a✝) (α_def ▸ ℓ)
⊢ evaluate (↑MG) X τ

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ : Formula
τ_in : τ ∈ F (?'a✝) (α_def ▸ ℓ)
⊢ evaluate (↑MG) X τ
Tactic:
have forTermination : lengthOfFormula τ < lengthOfProgram _ := F_goes_down τ_in
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ : Formula
τ_in : τ ∈ F (?'a✝) (α_def ▸ ℓ)
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
⊢ evaluate (↑MG) X τ

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ : Formula
τ_in : τ ∈ F (?'a✝) (α_def ▸ ℓ)
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
⊢ evaluate (↑MG) X τ
Tactic:
have := loadedTruthLemma MG X τ
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ : Formula
τ_in : τ ∈ F (?'a✝) (α_def ▸ ℓ)
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
this : (τ ∈ ↑X → evaluate (↑MG) X τ) ∧ ((~τ) ∈ ↑X → ¬evaluate (↑MG) X τ)
⊢ evaluate (↑MG) X τ

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ : Formula
τ_in : τ ∈ F (?'a✝) (α_def ▸ ℓ)
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
this : (τ ∈ ↑X → evaluate (↑MG) X τ) ∧ ((~τ) ∈ ↑X → ¬evaluate (↑MG) X τ)
⊢ evaluate (↑MG) X τ
Tactic:
subst α_def
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
τ : Formula
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
this : (τ ∈ ↑X → evaluate (↑MG) X τ) ∧ ((~τ) ∈ ↑X → ¬evaluate (↑MG) X τ)
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑X
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ_in : τ ∈ F (?'a✝) (⋯ ▸ ℓ)
⊢ evaluate (↑MG) X τ

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
τ : Formula
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
this : (τ ∈ ↑X → evaluate (↑MG) X τ) ∧ ((~τ) ∈ ↑X → ¬evaluate (↑MG) X τ)
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑X
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ_in : τ ∈ F (?'a✝) (⋯ ▸ ℓ)
⊢ evaluate (↑MG) X τ
Tactic:
simp_all only [instBot, relate, Subtype.exists, lengthOfProgram, true_or, forall_true_left]
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
⊢ (↑MG, X)⊨Con (F (?'a✝) (α_def ▸ ℓ))
Tactic:
simp [modelCanSemImplyForm,conEval]
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
⊢ ∀ f ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X f

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
⊢ ∀ f ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X f
Tactic:
exact X_F
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
⊢ (⌈⌈δ⌉⌉φ) ∈ ↑X
Tactic:
simp_all only [instBot, relate, Subtype.exists]
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
ℓ : TP α
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ Y Y
⊢ (⌈⌈δ⌉⌉φ) ∈ ↑Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
ℓ : TP α
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ Y Y
⊢ (⌈⌈δ⌉⌉φ) ∈ ↑Y
Tactic:
subst_eqs
State after:
case refl
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ (⌈⌈δ⌉⌉φ) ∈ ↑Y

State before:
case refl
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ (⌈⌈δ⌉⌉φ) ∈ ↑Y
Tactic:
apply Xset_sub_X
State after:
case refl.a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ (⌈⌈δ⌉⌉φ) ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = ⌈⌈δ⌉⌉φ

State before:
case refl.a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ (⌈⌈δ⌉⌉φ) ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = ⌈⌈δ⌉⌉φ
Tactic:
right
State after:
case refl.a.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = ⌈⌈δ⌉⌉φ

State before:
case refl.a.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = ⌈⌈δ⌉⌉φ
Tactic:
use δ
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
⊢ ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
Tactic:
intro d d_in_δ X' Y' φ' dφ_in_X' X'_d_Y'
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
⊢ φ' ∈ ↑Y'

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
⊢ φ' ∈ ↑Y'
Tactic:
have forTermination : lengthOf d < lengthOf α := by
  have := P_goes_down d_in_δ δ_in_P
  simp_all [isAtomic, isStar]
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
forTermination : lengthOf d < lengthOf α
⊢ φ' ∈ ↑Y'

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
forTermination : lengthOf d < lengthOf α
⊢ φ' ∈ ↑Y'
Tactic:
exact loadedTruthLemmaProg MG d X' φ' dφ_in_X' Y' X'_d_Y'
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
⊢ lengthOf d < lengthOf α
Tactic:
have := P_goes_down d_in_δ δ_in_P
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
this :
  if isAtomic (?'a✝) = true then d = (?'a✝)
  else
    if isStar (?'a✝) = true then lengthOfProgram d ≤ lengthOfProgram (?'a✝)
    else lengthOfProgram d < lengthOfProgram (?'a✝)
⊢ lengthOf d < lengthOf α

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
this :
  if isAtomic (?'a✝) = true then d = (?'a✝)
  else
    if isStar (?'a✝) = true then lengthOfProgram d ≤ lengthOfProgram (?'a✝)
    else lengthOfProgram d < lengthOfProgram (?'a✝)
⊢ lengthOf d < lengthOf α
Tactic:
simp_all [isAtomic, isStar]
State after:
no goals

State before:
case test.intro.intro.intro.inl
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
h✝ : δ = []
⊢ φ ∈ ↑Y
Tactic:
simp_all [relateSeq]
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
⊢ φ ∈ ↑Y
Tactic:
have := relateSeq_toChain' X_δ_Y δ_notEmpty
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
this : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ φ ∈ ↑Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
this : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ φ ∈ ↑Y
Tactic:
rcases this with ⟨l, length_def, lchain⟩
State after:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ φ ∈ ↑Y

State before:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ φ ∈ ↑Y
Tactic:
suffices loadClaim : ∀ i : Fin (X :: l ++ [Y]).length,
    (⌈⌈δ.drop i⌉⌉φ) ∈ ((X :: l ++ [Y]).get i).val by
  specialize loadClaim (Fin.last _)
  simp [length_def] at loadClaim
  convert loadClaim
  have := @List.get_last _ Y (X :: l) (Fin.last _)
  simp_all [eq_comm]
State after:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ ∀ (i : Fin (X :: l ++ [Y]).length), (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)

State before:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ ∀ (i : Fin (X :: l ++ [Y]).length), (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
Tactic:
intro i
State after:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
i : Fin (X :: l ++ [Y]).length
⊢ (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)

State before:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
i : Fin (X :: l ++ [Y]).length
⊢ (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
Tactic:
exact loadClaimHelper length_def δφ_in_X lchain IHδ i
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : ∀ (i : Fin (X :: l ++ [Y]).length), (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
⊢ φ ∈ ↑Y
Tactic:
specialize loadClaim (Fin.last _)
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim :
  (⌈⌈List.drop (↑(Fin.last (l.append [Y]).length)) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get (Fin.last (l.append [Y]).length))
⊢ φ ∈ ↑Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim :
  (⌈⌈List.drop (↑(Fin.last (l.append [Y]).length)) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get (Fin.last (l.append [Y]).length))
⊢ φ ∈ ↑Y
Tactic:
simp [length_def] at loadClaim
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
⊢ φ ∈ ↑Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
⊢ φ ∈ ↑Y
Tactic:
convert loadClaim
State after:
case h.e'_5.h.e'_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
⊢ Y = (X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length)

State before:
case h.e'_5.h.e'_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
⊢ Y = (X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length)
Tactic:
have := @List.get_last _ Y (X :: l) (Fin.last _)
State after:
case h.e'_5.h.e'_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
this : ¬↑(Fin.last (l.append [Y]).length) < (X :: l).length → (X :: l ++ [Y]).get (Fin.last (l.append [Y]).length) = Y
⊢ Y = (X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length)

State before:
case h.e'_5.h.e'_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
this : ¬↑(Fin.last (l.append [Y]).length) < (X :: l).length → (X :: l ++ [Y]).get (Fin.last (l.append [Y]).length) = Y
⊢ Y = (X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length)
Tactic:
simp_all [eq_comm]
State after:
no goals