Theorem: LO.Propositional.Superintuitionistic.Kripke.disjunctive_int
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.right.left
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
Fp : Frame' α
left✝¹ : Fp ∈ 𝔽(𝗘𝗙𝗤)
Vp : Valuation Fp.World α
hVp : ∀ {w₁ w₂ : Fp.World}, w₁ ≺ w₂ → ∀ {a : α}, Vp w₁ a → Vp w₂ a
wp : { Frame := Fp, Valuation := Vp, hereditary := ⋯ }.World
hp : ¬Satisfies { Frame := Fp, Valuation := Vp, hereditary := ⋯ } wp p
Fq : Frame' α
left✝ : Fq ∈ 𝔽(𝗘𝗙𝗤)
Vq : Valuation Fq.World α
hVq : ∀ {w₁ w₂ : Fq.World}, w₁ ≺ w₂ → ∀ {a : α}, Vq w₁ a → Vq w₂ a
wq : { Frame := Fq, Valuation := Vq, hereditary := ⋯ }.World
hq : ¬Satisfies { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wq q
M : Model α :=
  IntDPCounterexampleModel { Frame := Fp, Valuation := Vp, hereditary := ⋯ }
    { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wp wq
⊢ ¬Satisfies { Frame := M.Frame, Valuation := M.Valuation, hereditary := ⋯ } (Sum.inl ()) p

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.right.right
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
Fp : Frame' α
left✝¹ : Fp ∈ 𝔽(𝗘𝗙𝗤)
Vp : Valuation Fp.World α
hVp : ∀ {w₁ w₂ : Fp.World}, w₁ ≺ w₂ → ∀ {a : α}, Vp w₁ a → Vp w₂ a
wp : { Frame := Fp, Valuation := Vp, hereditary := ⋯ }.World
hp : ¬Satisfies { Frame := Fp, Valuation := Vp, hereditary := ⋯ } wp p
Fq : Frame' α
left✝ : Fq ∈ 𝔽(𝗘𝗙𝗤)
Vq : Valuation Fq.World α
hVq : ∀ {w₁ w₂ : Fq.World}, w₁ ≺ w₂ → ∀ {a : α}, Vq w₁ a → Vq w₂ a
wq : { Frame := Fq, Valuation := Vq, hereditary := ⋯ }.World
hq : ¬Satisfies { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wq q
M : Model α :=
  IntDPCounterexampleModel { Frame := Fp, Valuation := Vp, hereditary := ⋯ }
    { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wp wq
⊢ ¬Satisfies { Frame := M.Frame, Valuation := M.Valuation, hereditary := ⋯ } (Sum.inl ()) q
Tactic:
. exact not_imp_not.mpr (Satisfies.formula_hereditary (by apply Fp.Rel_refl)) $ satisfies_left_on_IntDPCounterexampleModel.not.mp hp;
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.right.right
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
Fp : Frame' α
left✝¹ : Fp ∈ 𝔽(𝗘𝗙𝗤)
Vp : Valuation Fp.World α
hVp : ∀ {w₁ w₂ : Fp.World}, w₁ ≺ w₂ → ∀ {a : α}, Vp w₁ a → Vp w₂ a
wp : { Frame := Fp, Valuation := Vp, hereditary := ⋯ }.World
hp : ¬Satisfies { Frame := Fp, Valuation := Vp, hereditary := ⋯ } wp p
Fq : Frame' α
left✝ : Fq ∈ 𝔽(𝗘𝗙𝗤)
Vq : Valuation Fq.World α
hVq : ∀ {w₁ w₂ : Fq.World}, w₁ ≺ w₂ → ∀ {a : α}, Vq w₁ a → Vq w₂ a
wq : { Frame := Fq, Valuation := Vq, hereditary := ⋯ }.World
hq : ¬Satisfies { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wq q
M : Model α :=
  IntDPCounterexampleModel { Frame := Fp, Valuation := Vp, hereditary := ⋯ }
    { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wp wq
⊢ ¬Satisfies { Frame := M.Frame, Valuation := M.Valuation, hereditary := ⋯ } (Sum.inl ()) q