Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p✝ q✝ : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p q : Formula α
ihp : ∀ {w : M₂.World}, Satisfies M₂ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p
ihq : ∀ {w : M₂.World}, Satisfies M₂ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q
w : M₂.World
h : ∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q
X : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
hWX :
  match Sum.inr (Sum.inr w), X with
  | Sum.inl val, Sum.inl val_1 => True
  | Sum.inl val, Sum.inr (Sum.inl v) => w₁ ≺ v
  | Sum.inl val, Sum.inr (Sum.inr v) => w₂ ≺ v
  | Sum.inr (Sum.inl w), Sum.inr (Sum.inl v) => w ≺ v
  | Sum.inr (Sum.inr w), Sum.inr (Sum.inr v) => w ≺ v
  | x, x_1 => False
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inr x) = X
Tactic:
split at hWX
Proof state after:
case h_1
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p✝ q✝ : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p q : Formula α
ihp : ∀ {w : M₂.World}, Satisfies M₂ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p
ihq : ∀ {w : M₂.World}, Satisfies M₂ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q
w : M₂.World
h : ∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q
w✝ v✝ : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World
val✝¹ val✝ : Unit
heq✝ : Sum.inr (Sum.inr w) = Sum.inl val✝¹
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inl val✝) p
hWX : True
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inr x) = Sum.inl val✝

case h_2
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p✝ q✝ : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p q : Formula α
ihp : ∀ {w : M₂.World}, Satisfies M₂ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p
ihq : ∀ {w : M₂.World}, Satisfies M₂ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q
w : M₂.World
h : ∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q
w✝ v✝¹ : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World
val✝ : Unit
v✝ : M₁.Frame.World
heq✝ : Sum.inr (Sum.inr w) = Sum.inl val✝
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl v✝)) p
hWX : w₁ ≺ v✝
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inr x) = Sum.inr (Sum.inl v✝)

case h_3
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p✝ q✝ : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p q : Formula α
ihp : ∀ {w : M₂.World}, Satisfies M₂ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p
ihq : ∀ {w : M₂.World}, Satisfies M₂ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q
w : M₂.World
h : ∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q
w✝ v✝¹ : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World
val✝ : Unit
v✝ : M₂.Frame.World
heq✝ : Sum.inr (Sum.inr w) = Sum.inl val✝
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr v✝)) p
hWX : w₂ ≺ v✝
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inr x) = Sum.inr (Sum.inr v✝)

case h_4
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p✝ q✝ : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p q : Formula α
ihp : ∀ {w : M₂.World}, Satisfies M₂ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p
ihq : ∀ {w : M₂.World}, Satisfies M₂ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q
w : M₂.World
h : ∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q
w✝¹ v✝¹ : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World
w✝ v✝ : M₁.Frame.World
heq✝ : Sum.inr (Sum.inr w) = Sum.inr (Sum.inl w✝)
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl v✝)) p
hWX : w✝ ≺ v✝
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inr x) = Sum.inr (Sum.inl v✝)

case h_5
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p✝ q✝ : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p q : Formula α
ihp : ∀ {w : M₂.World}, Satisfies M₂ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p
ihq : ∀ {w : M₂.World}, Satisfies M₂ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q
w : M₂.World
h : ∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q
w✝¹ v✝¹ : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World
w✝ v✝ : M₂.Frame.World
heq✝ : Sum.inr (Sum.inr w) = Sum.inr (Sum.inr w✝)
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr v✝)) p
hWX : w✝ ≺ v✝
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inr x) = Sum.inr (Sum.inr v✝)

case h_6
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p✝ q✝ : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p q : Formula α
ihp : ∀ {w : M₂.World}, Satisfies M₂ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p
ihq : ∀ {w : M₂.World}, Satisfies M₂ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q
w : M₂.World
h : ∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q
v✝¹ w✝ v✝ : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World
x✝⁴ : ∀ (val val_1 : Unit), Sum.inr (Sum.inr w) = Sum.inl val → v✝¹ = Sum.inl val_1 → False
x✝³ : ∀ (val : Unit) (v : M₁.Frame.World), Sum.inr (Sum.inr w) = Sum.inl val → v✝¹ = Sum.inr (Sum.inl v) → False
x✝² : ∀ (val : Unit) (v : M₂.Frame.World), Sum.inr (Sum.inr w) = Sum.inl val → v✝¹ = Sum.inr (Sum.inr v) → False
x✝¹ : ∀ (w_1 v : M₁.Frame.World), Sum.inr (Sum.inr w) = Sum.inr (Sum.inl w_1) → v✝¹ = Sum.inr (Sum.inl v) → False
x✝ : ∀ (w_1 v : M₂.Frame.World), Sum.inr (Sum.inr w) = Sum.inr (Sum.inr w_1) → v✝¹ = Sum.inr (Sum.inr v) → False
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) v✝¹ p
hWX : False
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inr x) = v✝¹