Theorem: LO.Propositional.Superintuitionistic.Kripke.disjunctive_int (Logic/Propositional/Superintuitionistic/Kripke/DP.lean)

State before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
⊢ 𝐈𝐧𝐭 ⊢! p ⋎ q → 𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q
Tactic:
contrapose
State after:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
⊢ ¬(𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q) → ¬𝐈𝐧𝐭 ⊢! p ⋎ q

State before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
⊢ ¬(𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q) → ¬𝐈𝐧𝐭 ⊢! p ⋎ q
Tactic:
intro hC
State after:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬(𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q)
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q

State before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬(𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q)
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q
Tactic:
push_neg at hC
State after:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q

State before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q
Tactic:
have ⟨hnp, hnq⟩ := hC
State after:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q

State before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q
Tactic:
obtain ⟨Fp, _, Vp, hVp, wp, hp⟩ := by simpa [ValidOnFrameClass, ValidOnFrame, ValidOnModel] using not_imp_not.mpr complete! hnp;
State after:
case intro.intro.intro.intro.intro
α : 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
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q

State before:
case intro.intro.intro.intro.intro
α : 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
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q
Tactic:
obtain ⟨Fq, _, Vq, hVq, wq, hq⟩ := by simpa [ValidOnFrameClass, ValidOnFrame, ValidOnModel] using not_imp_not.mpr complete! hnq;
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q
Tactic:
apply (not_imp_not.mpr sound!)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ q

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ q
Tactic:
simp [ValidOnFrameClass, ValidOnFrame, ValidOnModel]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ∃ x ∈ 𝔽(𝗘𝗙𝗤),
    ∃ x_1,
      ∃ (h : ∀ {w₁ w₂ : x.World}, w₁ ≺ w₂ → ∀ {a : α}, x_1 w₁ a → x_1 w₂ a),
        ∃ x_2,
          ¬Satisfies { Frame := x, Valuation := x_1, hereditary := ⋯ } x_2 p ∧
            ¬Satisfies { Frame := x, Valuation := x_1, hereditary := ⋯ } x_2 q

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ∃ x ∈ 𝔽(𝗘𝗙𝗤),
    ∃ x_1,
      ∃ (h : ∀ {w₁ w₂ : x.World}, w₁ ≺ w₂ → ∀ {a : α}, x_1 w₁ a → x_1 w₂ a),
        ∃ x_2,
          ¬Satisfies { Frame := x, Valuation := x_1, hereditary := ⋯ } x_2 p ∧
            ¬Satisfies { Frame := x, Valuation := x_1, hereditary := ⋯ } x_2 q
Tactic:
let M : Model α := IntDPCounterexampleModel ⟨Fp, Vp, hVp⟩ ⟨Fq, Vq, hVq⟩ wp wq
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ∃ x ∈ 𝔽(𝗘𝗙𝗤),
    ∃ x_1,
      ∃ (h : ∀ {w₁ w₂ : x.World}, w₁ ≺ w₂ → ∀ {a : α}, x_1 w₁ a → x_1 w₂ a),
        ∃ x_2,
          ¬Satisfies { Frame := x, Valuation := x_1, hereditary := ⋯ } x_2 p ∧
            ¬Satisfies { Frame := x, Valuation := x_1, hereditary := ⋯ } x_2 q

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ∃ x ∈ 𝔽(𝗘𝗙𝗤),
    ∃ x_1,
      ∃ (h : ∀ {w₁ w₂ : x.World}, w₁ ≺ w₂ → ∀ {a : α}, x_1 w₁ a → x_1 w₂ a),
        ∃ x_2,
          ¬Satisfies { Frame := x, Valuation := x_1, hereditary := ⋯ } x_2 p ∧
            ¬Satisfies { Frame := x, Valuation := x_1, hereditary := ⋯ } x_2 q
Tactic:
existsi M.Frame
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ M.Frame ∈ 𝔽(𝗘𝗙𝗤) ∧
    ∃ x,
      ∃ (h : ∀ {w₁ w₂ : M.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
        ∃ x_1,
          ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 p ∧
            ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 q

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ M.Frame ∈ 𝔽(𝗘𝗙𝗤) ∧
    ∃ x,
      ∃ (h : ∀ {w₁ w₂ : M.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
        ∃ x_1,
          ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 p ∧
            ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 q
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
⊢ M.Frame ∈ 𝔽(𝗘𝗙𝗤)

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
⊢ ∃ x,
    ∃ (h : ∀ {w₁ w₂ : M.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ∃ x_1,
        ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 p ∧
          ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 q

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
⊢ M.Frame ∈ 𝔽(𝗘𝗙𝗤)

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
⊢ ∃ x,
    ∃ (h : ∀ {w₁ w₂ : M.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ∃ x_1,
        ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 p ∧
          ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 q
Tactic:
. apply iff_definability_memAxiomSetFrameClass AxiomSet.EFQ.definability |>.mpr;
  trivial;
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
⊢ ∃ x,
    ∃ (h : ∀ {w₁ w₂ : M.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ∃ x_1,
        ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 p ∧
          ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 q

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
⊢ ∃ x,
    ∃ (h : ∀ {w₁ w₂ : M.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ∃ x_1,
        ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 p ∧
          ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 q
Tactic:
. existsi M.Valuation, M.hereditary, Sum.inl ();
  constructor;
  . exact not_imp_not.mpr (Satisfies.formula_hereditary (by apply Fp.Rel_refl)) $ satisfies_left_on_IntDPCounterexampleModel.not.mp hp;
  . exact not_imp_not.mpr (Satisfies.formula_hereditary (by apply Fq.Rel_refl)) $ satisfies_right_on_IntDPCounterexampleModel.not.mp hq;
State after:
no goals

State before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
⊢ ?m.380667
Tactic:
simpa [ValidOnFrameClass, ValidOnFrame, ValidOnModel] using not_imp_not.mpr complete! hnp
State after:
no goals

State before:
α : 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
⊢ ?m.515393
Tactic:
simpa [ValidOnFrameClass, ValidOnFrame, ValidOnModel] using not_imp_not.mpr complete! hnq
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
⊢ M.Frame ∈ 𝔽(𝗘𝗙𝗤)
Tactic:
apply iff_definability_memAxiomSetFrameClass AxiomSet.EFQ.definability |>.mpr
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
⊢ True

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
⊢ True
Tactic:
trivial
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
⊢ ∃ x,
    ∃ (h : ∀ {w₁ w₂ : M.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ∃ x_1,
        ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 p ∧
          ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 q
Tactic:
existsi M.Valuation, M.hereditary, Sum.inl ()
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 ()) p ∧
    ¬Satisfies { Frame := M.Frame, Valuation := M.Valuation, hereditary := ⋯ } (Sum.inl ()) q

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 ()) p ∧
    ¬Satisfies { Frame := M.Frame, Valuation := M.Valuation, hereditary := ⋯ } (Sum.inl ()) q
Tactic:
constructor
State after:
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

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;
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

State before:
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 Fq.Rel_refl)) $ satisfies_right_on_IntDPCounterexampleModel.not.mp hq;
State after:
no goals

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
Tactic:
exact not_imp_not.mpr (Satisfies.formula_hereditary (by apply Fp.Rel_refl)) $ satisfies_left_on_IntDPCounterexampleModel.not.mp hp
State after:
no goals

State before:
α : 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
⊢ Sum.inl () ≺ Sum.inr (Sum.inl wp)
Tactic:
apply Fp.Rel_refl
State after:
no goals

State before:
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 Fq.Rel_refl)) $ satisfies_right_on_IntDPCounterexampleModel.not.mp hq
State after:
no goals

State before:
α : 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
⊢ Sum.inl () ≺ Sum.inr (Sum.inr wq)
Tactic:
apply Fq.Rel_refl
State after:
no goals