Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem (Logic/Propositional/Superintuitionistic/Kripke/Semantics.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
⊢ M ⊧ Axioms.LEM p
Tactic:
simp_all [ValidOnModel]
State after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
⊢ ∀ (w : M.World), Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
⊢ ∀ (w : M.World), Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
intro w
State after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
by_cases h : w ⊧ p
State after:
case pos
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p

case neg
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p

State before:
case pos
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p

case neg
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
. left; assumption;
State after:
case neg
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p

State before:
case neg
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
. right;
  intro w' hww';
  rw [←(hExt hww')];
  assumption;
State after:
no goals

State before:
case pos
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
left
State after:
case pos.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : w ⊧ p
⊢ Satisfies M w p

State before:
case pos.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : w ⊧ p
⊢ Satisfies M w p
Tactic:
assumption
State after:
no goals

State before:
case neg
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
right
State after:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p

State before:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
intro w' hww'
State after:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ¬Satisfies M w' p

State before:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ¬Satisfies M w' p
Tactic:
rw [←(hExt hww')]
State after:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ¬Satisfies M w p

State before:
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ¬Satisfies M w p
Tactic:
assumption
State after:
no goals