internlm/Lean-Github huggingface dataset:
Theorem: LO.System.HenkinRule.henkin!
Proof state before:
F : Type u_1
inst✝⁸ : StandardModalLogicalConnective F
inst✝⁷ : DecidableEq F
S : Type u_2
inst✝⁶ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁵ : Classical 𝓢
inst✝⁴ : System.NegationEquiv 𝓢
inst✝³ : Necessitation 𝓢
inst✝² inst✝¹ : HasAxiomK 𝓢
inst✝ : HenkinRule 𝓢
⊢ 𝓢 ⊢! □p ⟷ p → 𝓢 ⊢! p
Tactic:
rintro ⟨hp⟩
Proof state after:
case intro
F : Type u_1
inst✝⁸ : StandardModalLogicalConnective F
inst✝⁷ : DecidableEq F
S : Type u_2
inst✝⁶ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁵ : Classical 𝓢
inst✝⁴ : System.NegationEquiv 𝓢
inst✝³ : Necessitation 𝓢
inst✝² inst✝¹ : HasAxiomK 𝓢
inst✝ : HenkinRule 𝓢
hp : 𝓢 ⊢ □p ⟷ p
⊢ 𝓢 ⊢! p
Theorem: LO.System.HenkinRule.henkin!
Proof state before:
case intro
F : Type u_1
inst✝⁸ : StandardModalLogicalConnective F
inst✝⁷ : DecidableEq F
S : Type u_2
inst✝⁶ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁵ : Classical 𝓢
inst✝⁴ : System.NegationEquiv 𝓢
inst✝³ : Necessitation 𝓢
inst✝² inst✝¹ : HasAxiomK 𝓢
inst✝ : HenkinRule 𝓢
hp : 𝓢 ⊢ □p ⟷ p
⊢ 𝓢 ⊢! p
Tactic:
exact ⟨henkin hp⟩
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_on_IntDPCounterexampleModel
Proof state before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
w w₁ : M₁.World
w₂ : M₂.World
⊢ Satisfies M₁ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl 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_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ Satisfies M₁ w (p ⟶ q) ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ Satisfies M₁ w (p ⟶ q) → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) (p ⟶ q) → Satisfies M₁ w (p ⟶ q)
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ Satisfies M₁ w (p ⟶ q) → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) (p ⟶ q) → Satisfies M₁ w (p ⟶ q)
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ Satisfies M₁ w (p ⟶ q) → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w) ≺ w' →
        Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' p → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' q
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl 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_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl 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.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w) ≺ X
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
x : M₁.Frame.World
hx : w ≺ x
ex : Sum.inr (Sum.inl x) = X
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X q
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w) ≺ X
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
x : M₁.Frame.World
hx : w ≺ x
ex : Sum.inr (Sum.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w) ≺ Sum.inr (Sum.inl x)
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl x)) p
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl x)) q
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w) ≺ Sum.inr (Sum.inl x)
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl x)) p
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl x)) q
Tactic:
exact ihq.mp $ h hx $ ihp.mpr hp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w) ≺ X
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w)) X
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inl x) = X
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w)) X
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl 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.inl x) = X
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w) = Sum.inl val → v✝¹ = Sum.inl val_1 → False
x✝³ : ∀ (val : Unit) (v : M₁.Frame.World), Sum.inr (Sum.inl w) = Sum.inl val → v✝¹ = Sum.inr (Sum.inl v) → False
x✝² : ∀ (val : Unit) (v : M₂.Frame.World), Sum.inr (Sum.inl w) = Sum.inl val → v✝¹ = Sum.inr (Sum.inr v) → False
x✝¹ : ∀ (w_1 v : M₁.Frame.World), Sum.inr (Sum.inl w) = Sum.inr (Sum.inl w_1) → v✝¹ = Sum.inr (Sum.inl v) → False
x✝ : ∀ (w_1 v : M₂.Frame.World), Sum.inr (Sum.inl 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.inl x) = v✝¹
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ (∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
      Sum.inr (Sum.inl 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_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ (∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
      Sum.inr (Sum.inl 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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
h :
  ∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
    Sum.inr (Sum.inl 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_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
h :
  ∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
    Sum.inr (Sum.inl 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_left_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.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
h :
  ∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
    Sum.inr (Sum.inl 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.inl w) ≺ Sum.inr (Sum.inl v)
Tactic:
simpa [IntDPCounterexampleModel]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.satisfies_left_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.inl w)) p✝
a✝ : ∀ {w : M₁.World}, Satisfies M₁ w q✝ ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q✝
w : M₁.World
⊢ Satisfies M₁ w (p✝ ⋎ q✝) ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) (p✝ ⋎ q✝)
Tactic:
simp_all [IntDPCounterexampleModel, Satisfies.iff_models, Satisfies]
Proof state after:
no goals