Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass (Logic/Modal/Standard/Kripke/Soundness.lean)

State before:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p : Formula α
d : L ⊢ p
⊢ 𝔽(Ax(L)) ⊧ p
Tactic:
induction d using Deduction.inducition_with_nec with
| hMaxm h => exact validOnAxiomSetFrameClass_axiom h;
| hMdp _ _ ihpq ihp =>
  intro F hF V w;
  exact Satisfies.mdp (ihpq F hF V w) (ihp F hF V w);
| hNec _ ih =>
  intro F hF V w w' _;
  exact ih F hF V w';
| hDisj₃ =>
  simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel];
  intros; rename_i hpr hqr hpq;
  cases hpq with
  | inl hp => exact hpr hp;
  | inr hq => exact hqr hq;
| _ => simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel];
State after:
no goals

State before:
case hMaxm
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
h : p✝ ∈ Ax(L)
⊢ 𝔽(Ax(L)) ⊧ p✝
Tactic:
exact validOnAxiomSetFrameClass_axiom h
State after:
no goals

State before:
case hMdp
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ : Formula α
hpq✝ : L ⊢ p✝ ⟶ q✝
hp✝ : L ⊢ p✝
ihpq : 𝔽(Ax(L)) ⊧ p✝ ⟶ q✝
ihp : 𝔽(Ax(L)) ⊧ p✝
⊢ 𝔽(Ax(L)) ⊧ q✝
Tactic:
intro F hF V w
State after:
case hMdp
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ : Formula α
hpq✝ : L ⊢ p✝ ⟶ q✝
hp✝ : L ⊢ p✝
ihpq : 𝔽(Ax(L)) ⊧ p✝ ⟶ q✝
ihp : 𝔽(Ax(L)) ⊧ p✝
F : Frame' α
hF : F ∈ 𝔽(Ax(L))
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ w ⊧ q✝

State before:
case hMdp
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ : Formula α
hpq✝ : L ⊢ p✝ ⟶ q✝
hp✝ : L ⊢ p✝
ihpq : 𝔽(Ax(L)) ⊧ p✝ ⟶ q✝
ihp : 𝔽(Ax(L)) ⊧ p✝
F : Frame' α
hF : F ∈ 𝔽(Ax(L))
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ w ⊧ q✝
Tactic:
exact Satisfies.mdp (ihpq F hF V w) (ihp F hF V w)
State after:
no goals

State before:
case hNec
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
hp✝ : L ⊢ p✝
ih : 𝔽(Ax(L)) ⊧ p✝
⊢ 𝔽(Ax(L)) ⊧ □p✝
Tactic:
intro F hF V w w' _
State after:
case hNec
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
hp✝ : L ⊢ p✝
ih : 𝔽(Ax(L)) ⊧ p✝
F : Frame' α
hF : F ∈ 𝔽(Ax(L))
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
w' : { Frame := F, Valuation := V }.Frame.World
a✝ : w ≺ w'
⊢ Satisfies { Frame := F, Valuation := V } w' p✝

State before:
case hNec
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
hp✝ : L ⊢ p✝
ih : 𝔽(Ax(L)) ⊧ p✝
F : Frame' α
hF : F ∈ 𝔽(Ax(L))
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
w' : { Frame := F, Valuation := V }.Frame.World
a✝ : w ≺ w'
⊢ Satisfies { Frame := F, Valuation := V } w' p✝
Tactic:
exact ih F hF V w'
State after:
no goals

State before:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
⊢ 𝔽(Ax(L)) ⊧ (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel]
State after:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
⊢ ∀ F ∈ 𝔽(Ax(L)),
    ∀ (V : Valuation F.World α) (w : { Frame := F, Valuation := V }.World),
      (Satisfies { Frame := F, Valuation := V } w p✝ → Satisfies { Frame := F, Valuation := V } w r✝) →
        (Satisfies { Frame := F, Valuation := V } w q✝ → Satisfies { Frame := F, Valuation := V } w r✝) →
          Satisfies { Frame := F, Valuation := V } w p✝ ∨ Satisfies { Frame := F, Valuation := V } w q✝ →
            Satisfies { Frame := F, Valuation := V } w r✝

State before:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
⊢ ∀ F ∈ 𝔽(Ax(L)),
    ∀ (V : Valuation F.World α) (w : { Frame := F, Valuation := V }.World),
      (Satisfies { Frame := F, Valuation := V } w p✝ → Satisfies { Frame := F, Valuation := V } w r✝) →
        (Satisfies { Frame := F, Valuation := V } w q✝ → Satisfies { Frame := F, Valuation := V } w r✝) →
          Satisfies { Frame := F, Valuation := V } w p✝ ∨ Satisfies { Frame := F, Valuation := V } w q✝ →
            Satisfies { Frame := F, Valuation := V } w r✝
Tactic:
intros
State after:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝³ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
a✝² : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
a✝¹ : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
a✝ : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ ∨ Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝

State before:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝³ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
a✝² : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
a✝¹ : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
a✝ : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ ∨ Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
Tactic:
rename_i hpr hqr hpq
State after:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
hpr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hqr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hpq : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ ∨ Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝

State before:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
hpr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hqr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hpq : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ ∨ Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
Tactic:
cases hpq with
| inl hp => exact hpr hp;
| inr hq => exact hqr hq;
State after:
no goals

State before:
case hDisj₃.inl
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
hpr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hqr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hp : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
Tactic:
exact hpr hp
State after:
no goals

State before:
case hDisj₃.inr
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
hpr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hqr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hq : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
Tactic:
exact hqr hq
State after:
no goals

State before:
case hDne
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
⊢ 𝔽(Ax(L)) ⊧ ~~p✝ ⟶ p✝
Tactic:
simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel]
State after:
no goals