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

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

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' → Satisfies M w' p → ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 q → Satisfies M w'_1 p
Tactic:
intro w₁ w₂ _ hp w₃ hw₂₃ _
State after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝¹ : w₁ ≺ w₂
hp : Satisfies M w₂ p
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
a✝ : Satisfies M w₃ q
⊢ Satisfies M w₃ p

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝¹ : w₁ ≺ w₂
hp : Satisfies M w₂ p
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
a✝ : Satisfies M w₃ q
⊢ Satisfies M w₃ p
Tactic:
exact Satisfies.formula_hereditary hw₂₃ hp
State after:
no goals