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

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hpq : M ⊧ p ⟶ q
hp : M ⊧ p
⊢ M ⊧ q
Tactic:
simp_all [ValidOnModel]
State after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hpq : ∀ (w : M.World) {w' : M.Frame.World}, w ≺ w' → Satisfies M w' q
hp : ∀ (w : M.World), Satisfies M w p
⊢ ∀ (w : M.World), Satisfies M w q

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

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hpq : ∀ (w : M.World) {w' : M.Frame.World}, w ≺ w' → Satisfies M w' q
hp : ∀ (w : M.World), Satisfies M w p
w : M.World
⊢ Satisfies M w q
Tactic:
exact hpq _ (M.Frame.Rel_refl w)
State after:
no goals