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

State before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hpq : F ⊧ p ⟶ q
hp : F ⊧ p
⊢ F ⊧ q
Tactic:
simp_all only [ValidOnFrame.models_iff, ValidOnFrame, ValidOnModel.iff_models]
State after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hpq :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q)
hp :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } p
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } q

State before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hpq :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q)
hp :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } p
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } q
Tactic:
intros V hV
State after:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hpq :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q)
hp :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } p
V : Valuation F.World α
hV : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V, hereditary := hV } q

State before:
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
hpq :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } (p ⟶ q)
hp :
  ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } p
V : Valuation F.World α
hV : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V, hereditary := hV } q
Tactic:
exact ValidOnModel.mdp (hpq V hV) (hp V hV)
State after:
no goals