internlm/Lean-Github huggingface dataset:
Theorem: localRuleTruth
Proof 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.inl none with
      | none => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
      (L ++ X, R, some (Sum.inl (~'χ)))
Tactic:
simp only [Option.map_none', and_true]
Proof 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
Theorem: localRuleTruth
Proof 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
Tactic:
exact in_ress
Proof state after:
no goals
Theorem: localRuleTruth
Proof 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 ++ X, R, some (Sum.inl (~'χ)))
Tactic:
intro g
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Theorem: localRuleTruth
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Tactic:
subst def_f
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Theorem: localRuleTruth
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Tactic:
rw [conEval] at w_f
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Theorem: localRuleTruth
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Tactic:
specialize hyp g
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Theorem: localRuleTruth
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Tactic:
aesop
Proof state after:
no goals
Theorem: localRuleTruth
Proof 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.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
use (L ++ X, R, some (Sum.inl val))
Proof 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.inl b with
          | none => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
          (L ++ X, R, some (Sum.inl val))) ∧
    (M, w)⊨(L ++ X, R, some (Sum.inl val))
Theorem: localRuleTruth
Proof 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.inl b with
          | none => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
          (L ++ X, R, some (Sum.inl val))) ∧
    (M, w)⊨(L ++ X, R, some (Sum.inl val))
Tactic:
constructor
Proof 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.inl b with
        | none => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
        (L ++ X, R, some (Sum.inl 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 ++ X, R, some (Sum.inl val))
Theorem: localRuleTruth
Proof 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.inl b with
        | none => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
        (L ++ X, R, some (Sum.inl val))
Tactic:
use X, some val
Proof 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.inl (some val) with
      | none => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
      (L ++ X, R, some (Sum.inl val))
Theorem: localRuleTruth
Proof 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.inl (some val) with
      | none => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
      (L ++ X, R, some (Sum.inl val))
Tactic:
simp only [Option.map_some', and_true]
Proof 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
Theorem: localRuleTruth
Proof 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
Tactic:
exact in_ress
Proof state after:
no goals
Theorem: localRuleTruth
Proof 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 ++ X, R, some (Sum.inl val))
Tactic:
intro g g_in
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g
Theorem: localRuleTruth
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g
Tactic:
subst def_f
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
w_f : evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))
⊢ evaluate M w g
Theorem: localRuleTruth
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl 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
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
⊢ evaluate M w g
Theorem: localRuleTruth
Proof 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 ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl 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
Proof 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 ∈ X) ∨ g ∈ R) ∨ g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g
Theorem: localRuleTruth
Proof 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 ∈ X) ∨ g ∈ R) ∨ g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g
Tactic:
rcases g_in with ((g_in|g_in)|g_in)|g_in
Proof state after:
case h.right.inl.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.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
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.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
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.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.inl val))).toList
⊢ evaluate M w g