internlm/Lean-Github huggingface dataset:
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
w₂ : M₂.World
⊢ Satisfies M₂ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p
Tactic:
induction p using rec' generalizing w with
| himp p q ihp ihq =>
  constructor;
  . simp only [Satisfies.imp_def];
    intro h X hWX hp;
    obtain ⟨x, hx, ex⟩ : ∃ x, w ≺ x ∧ (Sum.inr $ Sum.inr x) = X := by
      replace hWX : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Frame.Rel _ X := hWX;
      simp [IntDPCounterexampleFrame] at hWX;
      split at hWX;
      all_goals simp_all;
    subst ex;
    exact ihq.mp $ h hx $ ihp.mpr hp;
  . simp only [Satisfies.imp_def];
    intro h v hv hp;
    exact ihq.mpr $ h (by simpa [IntDPCounterexampleModel]) $ ihp.mp hp;
| _ => simp_all [IntDPCounterexampleModel, Satisfies.iff_models, Satisfies];
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp
α : 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
⊢ Satisfies M₂ w (p ⟶ q) ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q)
Tactic:
constructor
Proof state after:
case himp.mp
α : 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
⊢ Satisfies M₂ w (p ⟶ q) → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q)

case himp.mpr
α : 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
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q) → Satisfies M₂ w (p ⟶ q)
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp.mp
α : 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
⊢ Satisfies M₂ w (p ⟶ q) → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q)

case himp.mpr
α : 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
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q) → Satisfies M₂ w (p ⟶ q)
Tactic:
. simp only [Satisfies.imp_def];
  intro h X hWX hp;
  obtain ⟨x, hx, ex⟩ : ∃ x, w ≺ x ∧ (Sum.inr $ Sum.inr x) = X := by
    replace hWX : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Frame.Rel _ X := hWX;
    simp [IntDPCounterexampleFrame] at hWX;
    split at hWX;
    all_goals simp_all;
  subst ex;
  exact ihq.mp $ h hx $ ihp.mpr hp;
Proof state after:
case himp.mpr
α : 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
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q) → Satisfies M₂ w (p ⟶ q)
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp.mpr
α : 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
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q) → Satisfies M₂ w (p ⟶ q)
Tactic:
. simp only [Satisfies.imp_def];
  intro h v hv hp;
  exact ihq.mpr $ h (by simpa [IntDPCounterexampleModel]) $ ihp.mp hp;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp.mp
α : 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
⊢ Satisfies M₂ w (p ⟶ q) → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q)
Tactic:
simp only [Satisfies.imp_def]
Proof state after:
case himp.mp
α : 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
⊢ (∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q) →
    ∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
      Sum.inr (Sum.inr w) ≺ w' →
        Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' p → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' q
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp.mp
α : 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
⊢ (∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q) →
    ∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
      Sum.inr (Sum.inr w) ≺ w' →
        Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' p → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' q
Tactic:
intro h X hWX hp
Proof state after:
case himp.mp
α : 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
hWX : Sum.inr (Sum.inr w) ≺ X
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X q
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp.mp
α : 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
hWX : Sum.inr (Sum.inr w) ≺ X
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X q
Tactic:
obtain ⟨x, hx, ex⟩ : ∃ x, w ≺ x ∧ (Sum.inr $ Sum.inr x) = X := by
  replace hWX : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Frame.Rel _ X := hWX;
  simp [IntDPCounterexampleFrame] at hWX;
  split at hWX;
  all_goals simp_all;
Proof state after:
case himp.mp.intro.intro
α : 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
hWX : Sum.inr (Sum.inr w) ≺ X
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
x : M₂.Frame.World
hx : w ≺ x
ex : Sum.inr (Sum.inr x) = X
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X q
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp.mp.intro.intro
α : 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
hWX : Sum.inr (Sum.inr w) ≺ X
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
x : M₂.Frame.World
hx : w ≺ x
ex : Sum.inr (Sum.inr x) = X
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X q
Tactic:
subst ex
Proof state after:
case himp.mp.intro.intro
α : 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 : M₂.Frame.World
hx : w ≺ x
hWX : Sum.inr (Sum.inr w) ≺ Sum.inr (Sum.inr x)
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr x)) p
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr x)) q
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp.mp.intro.intro
α : 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 : M₂.Frame.World
hx : w ≺ x
hWX : Sum.inr (Sum.inr w) ≺ Sum.inr (Sum.inr x)
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr x)) p
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr x)) q
Tactic:
exact ihq.mp $ h hx $ ihp.mpr hp
Proof state after:
no goals
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
hWX : Sum.inr (Sum.inr w) ≺ X
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inr x) = X
Tactic:
replace hWX : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Frame.Rel _ X := hWX
Proof state after:
α : 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 : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Frame.Rel (Sum.inr (Sum.inr w)) X
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inr x) = X
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 : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Frame.Rel (Sum.inr (Sum.inr w)) X
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inr x) = X
Tactic:
simp [IntDPCounterexampleFrame] at hWX
Proof state after:
α : 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
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
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✝¹
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp.mpr
α : 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
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q) → Satisfies M₂ w (p ⟶ q)
Tactic:
simp only [Satisfies.imp_def]
Proof state after:
case himp.mpr
α : 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
⊢ (∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
      Sum.inr (Sum.inr w) ≺ w' →
        Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' p → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' q) →
    ∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp.mpr
α : 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
⊢ (∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
      Sum.inr (Sum.inr w) ≺ w' →
        Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' p → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' q) →
    ∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' q
Tactic:
intro h v hv hp
Proof state after:
case himp.mpr
α : 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' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
    Sum.inr (Sum.inr w) ≺ w' →
      Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' p → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' q
v : M₂.Frame.World
hv : w ≺ v
hp : Satisfies M₂ v p
⊢ Satisfies M₂ v q
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case himp.mpr
α : 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' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
    Sum.inr (Sum.inr w) ≺ w' →
      Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' p → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' q
v : M₂.Frame.World
hv : w ≺ v
hp : Satisfies M₂ v p
⊢ Satisfies M₂ v q
Tactic:
exact ihq.mpr $ h (by simpa [IntDPCounterexampleModel]) $ ihp.mp hp
Proof state after:
no goals
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' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
    Sum.inr (Sum.inr w) ≺ w' →
      Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' p → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' q
v : M₂.Frame.World
hv : w ≺ v
hp : Satisfies M₂ v p
⊢ Sum.inr (Sum.inr w) ≺ Sum.inr (Sum.inr v)
Tactic:
simpa [IntDPCounterexampleModel]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_right_on_IntDPCounterexampleModel
Proof state before:
case hor
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p✝ q✝ : Formula α
a✝¹ : ∀ {w : M₂.World}, Satisfies M₂ w p✝ ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p✝
a✝ : ∀ {w : M₂.World}, Satisfies M₂ w q✝ ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q✝
w : M₂.World
⊢ Satisfies M₂ w (p✝ ⋎ q✝) ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p✝ ⋎ q✝)
Tactic:
simp_all [IntDPCounterexampleModel, Satisfies.iff_models, Satisfies]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.disjunctive_int
Proof state before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
⊢ 𝐈𝐧𝐭 ⊢! p ⋎ q → 𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q
Tactic:
contrapose
Proof state after:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
⊢ ¬(𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q) → ¬𝐈𝐧𝐭 ⊢! p ⋎ q
Theorem: LO.Propositional.Superintuitionistic.Kripke.disjunctive_int
Proof state before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
⊢ ¬(𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q) → ¬𝐈𝐧𝐭 ⊢! p ⋎ q
Tactic:
intro hC
Proof state after:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬(𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q)
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q
Theorem: LO.Propositional.Superintuitionistic.Kripke.disjunctive_int
Proof 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
Proof state after:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q