Theorem: localRuleTruth (Pdl/LocalTableau.lean)

State before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
have hyp' := hyp (~unload χ)
State after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ((~unload χ) ∈ L ∨ (~unload χ) ∈ R) ∨ (~unload χ) = (~unload χ) → evaluate M w (~unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ((~unload χ) ∈ L ∨ (~unload χ) ∈ R) ∨ (~unload χ) = (~unload χ) → evaluate M w (~unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
simp at hyp'
State after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ¬evaluate M w (unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ¬evaluate M w (unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
rw [this] at hyp'
State after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
rcases hyp' with ⟨f, ⟨X , O, in_ress, def_f⟩, w_f⟩
State after:
case mp.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_f : Con (X ++ (Option.map negUnload O).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_f : Con (X ++ (Option.map negUnload O).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
cases O
State after:
case mp.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

case mp.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val✝)).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
use (L, R ++ X, some (Sum.inr (~'χ)))
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inr b with
          | none => (L, R ++ a, some (Sum.inr (~'χ)))
          | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
          (L, R ++ X, some (Sum.inr (~'χ)))) ∧
    (M, w)⊨(L, R ++ X, some (Sum.inr (~'χ)))

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inr b with
          | none => (L, R ++ a, some (Sum.inr (~'χ)))
          | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
          (L, R ++ X, some (Sum.inr (~'χ)))) ∧
    (M, w)⊨(L, R ++ X, some (Sum.inr (~'χ)))
Tactic:
constructor
State after:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ a b,
    (a, b) ∈ ress ∧
      (match Option.map Sum.inr b with
        | none => (L, R ++ a, some (Sum.inr (~'χ)))
        | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
        (L, R ++ X, some (Sum.inr (~'χ)))

case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (M, w)⊨(L, R ++ X, some (Sum.inr (~'χ)))

State before:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ a b,
    (a, b) ∈ ress ∧
      (match Option.map Sum.inr b with
        | none => (L, R ++ a, some (Sum.inr (~'χ)))
        | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
        (L, R ++ X, some (Sum.inr (~'χ)))
Tactic:
use X, none
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (X, none) ∈ ress ∧
    (match Option.map Sum.inr none with
      | none => (L, R ++ X, some (Sum.inr (~'χ)))
      | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))) =
      (L, R ++ X, some (Sum.inr (~'χ)))

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (X, none) ∈ ress ∧
    (match Option.map Sum.inr none with
      | none => (L, R ++ X, some (Sum.inr (~'χ)))
      | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))) =
      (L, R ++ X, some (Sum.inr (~'χ)))
Tactic:
simp only [Option.map_none', and_true]
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (X, none) ∈ ress

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (M, w)⊨(L, R ++ X, some (Sum.inr (~'χ)))
Tactic:
intro g
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
g : Formula
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
g : Formula
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w g
Tactic:
subst def_f
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : evaluate M w (Con (X ++ (Option.map negUnload none).toList))
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : evaluate M w (Con (X ++ (Option.map negUnload none).toList))
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w g
Tactic:
rw [conEval] at w_f
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload none).toList, evaluate M w f
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload none).toList, evaluate M w f
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w g
Tactic:
specialize hyp g
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload none).toList, evaluate M w f
hyp : (g ∈ L ∨ g ∈ R) ∨ (~unload χ) = g → evaluate M w g
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload none).toList, evaluate M w f
hyp : (g ∈ L ∨ g ∈ R) ∨ (~unload χ) = g → evaluate M w g
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w g
Tactic:
aesop
State after:
no goals

State before:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
use (L, R ++ X, some (Sum.inr val))
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inr b with
          | none => (L, R ++ a, some (Sum.inr (~'χ)))
          | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
          (L, R ++ X, some (Sum.inr val))) ∧
    (M, w)⊨(L, R ++ X, some (Sum.inr val))

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inr b with
          | none => (L, R ++ a, some (Sum.inr (~'χ)))
          | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
          (L, R ++ X, some (Sum.inr val))) ∧
    (M, w)⊨(L, R ++ X, some (Sum.inr val))
Tactic:
constructor
State after:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ ∃ a b,
    (a, b) ∈ ress ∧
      (match Option.map Sum.inr b with
        | none => (L, R ++ a, some (Sum.inr (~'χ)))
        | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
        (L, R ++ X, some (Sum.inr val))

case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (M, w)⊨(L, R ++ X, some (Sum.inr val))

State before:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ ∃ a b,
    (a, b) ∈ ress ∧
      (match Option.map Sum.inr b with
        | none => (L, R ++ a, some (Sum.inr (~'χ)))
        | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
        (L, R ++ X, some (Sum.inr val))
Tactic:
use X, some val
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (X, some val) ∈ ress ∧
    (match Option.map Sum.inr (some val) with
      | none => (L, R ++ X, some (Sum.inr (~'χ)))
      | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))) =
      (L, R ++ X, some (Sum.inr val))

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (X, some val) ∈ ress ∧
    (match Option.map Sum.inr (some val) with
      | none => (L, R ++ X, some (Sum.inr (~'χ)))
      | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))) =
      (L, R ++ X, some (Sum.inr val))
Tactic:
simp only [Option.map_some', and_true]
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (X, some val) ∈ ress

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (M, w)⊨(L, R ++ X, some (Sum.inr val))
Tactic:
intro g g_in
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
g : Formula
g_in : g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
⊢ evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
g : Formula
g_in : g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
⊢ evaluate M w g
Tactic:
subst def_f
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
g_in : g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
w_f : evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))
⊢ evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
g_in : g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
w_f : evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))
⊢ evaluate M w g
Tactic:
rw [conEval] at w_f
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
g_in : g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
⊢ evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
g_in : g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
⊢ evaluate M w g
Tactic:
simp only [List.mem_union_iff, List.mem_append, List.mem_singleton] at g_in
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : (g ∈ L ∨ g ∈ R ∨ g ∈ X) ∨ g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
⊢ evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : (g ∈ L ∨ g ∈ R ∨ g ∈ X) ∨ g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
⊢ evaluate M w g
Tactic:
rcases g_in with (g_in|(g_in|g_in))|g_in
State after:
case h.right.inl.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ L
⊢ evaluate M w g

case h.right.inl.inr.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ R
⊢ evaluate M w g

case h.right.inl.inr.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ X
⊢ evaluate M w g

case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
⊢ evaluate M w g

State before:
case h.right.inl.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ L
⊢ evaluate M w g

case h.right.inl.inr.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ R
⊢ evaluate M w g

case h.right.inl.inr.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ X
⊢ evaluate M w g

case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
⊢ evaluate M w g
Tactic:
all_goals aesop
State after:
no goals

State before:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
⊢ evaluate M w g
Tactic:
aesop
State after:
no goals

State before:
case mpr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inr b with
              | none => (L, R ++ a, some (Sum.inr (~'χ)))
              | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci) →
    ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
Tactic:
rintro ⟨Ci, ⟨⟨X, O, ⟨in_ress, def_Ci⟩⟩, w_Ci⟩⟩
State after:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
Ci : TNode
w_Ci : (M, w)⊨Ci
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_Ci :
  (match Option.map Sum.inr O with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))) =
    Ci
⊢ ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
Ci : TNode
w_Ci : (M, w)⊨Ci
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_Ci :
  (match Option.map Sum.inr O with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))) =
    Ci
⊢ ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
Tactic:
intro f f_in
State after:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
Ci : TNode
w_Ci : (M, w)⊨Ci
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_Ci :
  (match Option.map Sum.inr O with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))) =
    Ci
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
Ci : TNode
w_Ci : (M, w)⊨Ci
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_Ci :
  (match Option.map Sum.inr O with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))) =
    Ci
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
⊢ evaluate M w f
Tactic:
subst def_Ci
State after:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
w_Ci :
  (M, w)⊨match Option.map Sum.inr O with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
w_Ci :
  (M, w)⊨match Option.map Sum.inr O with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))
⊢ evaluate M w f
Tactic:
cases O
State after:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci :
  (M, w)⊨match Option.map Sum.inr none with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))
⊢ evaluate M w f

case mpr.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
w_Ci :
  (M, w)⊨match Option.map Sum.inr (some val✝) with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci :
  (M, w)⊨match Option.map Sum.inr none with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))
⊢ evaluate M w f

case mpr.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
w_Ci :
  (M, w)⊨match Option.map Sum.inr (some val✝) with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))
⊢ evaluate M w f
Tactic:
all_goals simp at *
State after:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'χ)))
⊢ evaluate M w f

case mpr.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val✝.1)))
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
w_Ci :
  (M, w)⊨match Option.map Sum.inr (some val✝) with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))
⊢ evaluate M w f
Tactic:
simp at *
State after:
case mpr.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val✝.1)))
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'χ)))
⊢ evaluate M w f
Tactic:
have := w_Ci f
State after:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this✝ :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'χ)))
this : f ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w f
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this✝ :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'χ)))
this : f ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w f
⊢ evaluate M w f
Tactic:
aesop
State after:
no goals

State before:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ evaluate M w f
Tactic:
rcases f_in with (f_in|f_in)|f_in
State after:
case inl.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
f_in : f ∈ L
⊢ evaluate M w f

case inl.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
f_in : f ∈ R
⊢ evaluate M w f

case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
f_in : (~unload χ) = f
⊢ evaluate M w f

State before:
case inl.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
f_in : f ∈ L
⊢ evaluate M w f
Tactic:
apply w_Ci
State after:
case inl.inl.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
f_in : f ∈ L
⊢ f ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'val.1)))).toList

State before:
case inl.inl.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
f_in : f ∈ L
⊢ f ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'val.1)))).toList
Tactic:
simp_all
State after:
no goals

State before:
case inl.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
f_in : f ∈ R
⊢ evaluate M w f
Tactic:
apply w_Ci
State after:
case inl.inr.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
f_in : f ∈ R
⊢ f ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'val.1)))).toList

State before:
case inl.inr.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
f_in : f ∈ R
⊢ f ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'val.1)))).toList
Tactic:
simp_all
State after:
no goals

State before:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
f_in : (~unload χ) = f
⊢ evaluate M w f
Tactic:
subst f_in
State after:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ evaluate M w (~unload χ)

State before:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ evaluate M w (~unload χ)
Tactic:
simp only [evaluate]
State after:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ ¬evaluate M w (unload χ)

State before:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ ¬evaluate M w (unload χ)
Tactic:
rw [this]
State after:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f

State before:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
Tactic:
use Con (X ++ Option.toList (Option.map negUnload (some val)))
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        Con (a ++ (Option.map negUnload b).toList) = Con (X ++ (Option.map negUnload (some val)).toList)) ∧
    evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        Con (a ++ (Option.map negUnload b).toList) = Con (X ++ (Option.map negUnload (some val)).toList)) ∧
    evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))
Tactic:
constructor
State after:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ ∃ a b,
    (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = Con (X ++ (Option.map negUnload (some val)).toList)

case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))

State before:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ ∃ a b,
    (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = Con (X ++ (Option.map negUnload (some val)).toList)
Tactic:
use X, some val
State after:
no goals

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))
Tactic:
rw [conEval]
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
Tactic:
simp only [Option.map_some', negUnload, Option.toList_some, List.mem_append, List.mem_singleton]
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ ∀ (f : Formula), f ∈ X ∨ f = (~unload val.1) → evaluate M w f

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ ∀ (f : Formula), f ∈ X ∨ f = (~unload val.1) → evaluate M w f
Tactic:
intro g g_in
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
g : Formula
g_in : g ∈ X ∨ g = (~unload val.1)
⊢ evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
g : Formula
g_in : g ∈ X ∨ g = (~unload val.1)
⊢ evaluate M w g
Tactic:
rcases g_in with (_|g_def)
State after:
case h.right.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
g : Formula
h✝ : g ∈ X
⊢ evaluate M w g

case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
g : Formula
g_def : g = (~unload val.1)
⊢ evaluate M w g

State before:
case h.right.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
g : Formula
h✝ : g ∈ X
⊢ evaluate M w g
Tactic:
apply w_Ci
State after:
case h.right.inl.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
g : Formula
h✝ : g ∈ X
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'val.1)))).toList

State before:
case h.right.inl.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
g : Formula
h✝ : g ∈ X
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'val.1)))).toList
Tactic:
simp_all
State after:
no goals

State before:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
g : Formula
g_def : g = (~unload val.1)
⊢ evaluate M w g
Tactic:
subst g_def
State after:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ evaluate M w (~unload val.1)

State before:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ evaluate M w (~unload val.1)
Tactic:
apply w_Ci
State after:
case h.right.inr.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ (~unload val.1) ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'val.1)))).toList

State before:
case h.right.inr.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ (~unload val.1) ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'val.1)))).toList
Tactic:
simp_all
State after:
no goals