internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚺 (s✝ + 1) p✝
ih : StrictHierarchy 𝚺 (s✝ + 1 + 1) p✝
⊢ StrictHierarchy 𝚺 (s✝ + 1 + 1) (∃' p✝)
Tactic:
case ex ih => exact ih.ex
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
ih : StrictHierarchy 𝚷 (s✝ + 1 + 1) p✝
⊢ StrictHierarchy 𝚷 (s✝ + 1 + 1) (∀' p✝)
Tactic:
case all ih => exact ih.all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
x✝ s✝ : ℕ
Γ✝ : Polarity
p✝ : Semiformula L μ₁ x✝
h : DeltaZero p✝
⊢ StrictHierarchy Γ✝ (s✝ + 1) p✝
Tactic:
exact zero h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 s✝ p✝
ih : StrictHierarchy 𝚷 (s✝ + 1) p✝
⊢ StrictHierarchy 𝚺 (s✝ + 1 + 1) (∃' p✝)
Tactic:
exact ih.sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚺 s✝ p✝
ih : StrictHierarchy 𝚺 (s✝ + 1) p✝
⊢ StrictHierarchy 𝚷 (s✝ + 1 + 1) (∀' p✝)
Tactic:
exact ih.pi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚺 (s✝ + 1) p✝
ih : StrictHierarchy 𝚺 (s✝ + 1 + 1) p✝
⊢ StrictHierarchy 𝚺 (s✝ + 1 + 1) (∃' p✝)
Tactic:
exact ih.ex
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
ih : StrictHierarchy 𝚷 (s✝ + 1 + 1) p✝
⊢ StrictHierarchy 𝚷 (s✝ + 1 + 1) (∀' p✝)
Tactic:
exact ih.all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.zero_iff_delta_zero
Proof state before:
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ StrictHierarchy Γ 0 p ↔ DeltaZero p
Tactic:
constructor
Proof state after:
case mp
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ StrictHierarchy Γ 0 p → DeltaZero p

case mpr
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ DeltaZero p → StrictHierarchy Γ 0 p
Theorem: LO.FirstOrder.Arith.StrictHierarchy.zero_iff_delta_zero
Proof state before:
case mp
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ StrictHierarchy Γ 0 p → DeltaZero p
Tactic:
rintro ⟨h⟩
Proof state after:
case mp.zero
L : Language
inst✝ : L.LT
μ : Type u_1
n✝ : ℕ
Γ : Polarity
p : Semiformula L μ n✝
n : ℕ
h : DeltaZero p
⊢ DeltaZero p
Theorem: LO.FirstOrder.Arith.StrictHierarchy.zero_iff_delta_zero
Proof state before:
case mp.zero
L : Language
inst✝ : L.LT
μ : Type u_1
n✝ : ℕ
Γ : Polarity
p : Semiformula L μ n✝
n : ℕ
h : DeltaZero p
⊢ DeltaZero p
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.zero_iff_delta_zero
Proof state before:
case mpr
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ DeltaZero p → StrictHierarchy Γ 0 p
Tactic:
intro h
Proof state after:
case mpr
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
h : DeltaZero p
⊢ StrictHierarchy Γ 0 p
Theorem: LO.FirstOrder.Arith.StrictHierarchy.zero_iff_delta_zero
Proof state before:
case mpr
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
h : DeltaZero p
⊢ StrictHierarchy Γ 0 p
Tactic:
exact zero h
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.atom_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
w : M.World
a : α
⊢ Satisfies M w (atom a) ↔ M.Valuation w a
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.top_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
w : M.World
⊢ Satisfies M w ⊤ ↔ True
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.bot_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
w : M.World
⊢ Satisfies M w ⊥ ↔ False
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.and_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w (p ⋏ q) ↔ Satisfies M w p ∧ Satisfies M w q
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.or_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w (p ⋎ q) ↔ Satisfies M w p ∨ Satisfies M w q
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.imp_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w (p ⟶ q) ↔ ∀ {w' : M.Frame.World}, w ≺ w' → Satisfies M w' p → Satisfies M w' q
Tactic:
simp [Satisfies, imp_iff_not_or]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.neg_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
w : M.World
p : Formula α
⊢ Satisfies M w (~p) ↔ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
simp [NegAbbrev.neg]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.formula_hereditary
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
p : Formula α
hw : w ≺ w'
⊢ Satisfies M w p → Satisfies M w' p
Tactic:
induction p using Formula.rec' with
| hatom => apply M.hereditary hw;
| himp =>
  simp_all [Satisfies];
  intro hpq v hv;
  exact hpq $ M.Frame.Rel_trans hw hv;
| hor => simp_all [Satisfies]; tauto;
| _ => simp_all [Satisfies];
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.formula_hereditary
Proof state before:
case hatom
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
a✝ : α
⊢ Satisfies M w (atom a✝) → Satisfies M w' (atom a✝)
Tactic:
apply M.hereditary hw
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.formula_hereditary
Proof state before:
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w (p✝ ⟶ q✝) → Satisfies M w' (p✝ ⟶ q✝)
Tactic:
simp_all [Satisfies]
Proof state after:
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ (∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p✝ ∨ Satisfies M w' q✝) →
    ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → ¬Satisfies M w'_1 p✝ ∨ Satisfies M w'_1 q✝
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.formula_hereditary
Proof state before:
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ (∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p✝ ∨ Satisfies M w' q✝) →
    ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → ¬Satisfies M w'_1 p✝ ∨ Satisfies M w'_1 q✝
Tactic:
intro hpq v hv
Proof state after:
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
hpq : ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p✝ ∨ Satisfies M w' q✝
v : M.Frame.World
hv : w' ≺ v
⊢ ¬Satisfies M v p✝ ∨ Satisfies M v q✝
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.formula_hereditary
Proof state before:
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
hpq : ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p✝ ∨ Satisfies M w' q✝
v : M.Frame.World
hv : w' ≺ v
⊢ ¬Satisfies M v p✝ ∨ Satisfies M v q✝
Tactic:
exact hpq $ M.Frame.Rel_trans hw hv
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.formula_hereditary
Proof state before:
case hor
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w (p✝ ⋎ q✝) → Satisfies M w' (p✝ ⋎ q✝)
Tactic:
simp_all [Satisfies]
Proof state after:
case hor
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w p✝ ∨ Satisfies M w q✝ → Satisfies M w' p✝ ∨ Satisfies M w' q✝
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.formula_hereditary
Proof state before:
case hor
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w p✝ ∨ Satisfies M w q✝ → Satisfies M w' p✝ ∨ Satisfies M w' q✝
Tactic:
tauto
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.formula_hereditary
Proof state before:
case hand
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w (p✝ ⋏ q✝) → Satisfies M w' (p✝ ⋏ q✝)
Tactic:
simp_all [Satisfies]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.verum
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ ⊤
Tactic:
simp_all [ValidOnModel]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.conj₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ p ⋏ q ⟶ p
Tactic:
simp_all [ValidOnModel]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.conj₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ p ⋏ q ⟶ q
Tactic:
simp_all [ValidOnModel]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.conj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ p ⟶ q ⟶ p ⋏ q
Tactic:
simp_all [ValidOnModel]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' → Satisfies M w' p → ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 q → Satisfies M w'_1 p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.conj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' → Satisfies M w' p → ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 q → Satisfies M w'_1 p
Tactic:
intro w₁ w₂ _ hp w₃ hw₂₃ _
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝¹ : w₁ ≺ w₂
hp : Satisfies M w₂ p
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
a✝ : Satisfies M w₃ q
⊢ Satisfies M w₃ p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.conj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝¹ : w₁ ≺ w₂
hp : Satisfies M w₂ p
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
a✝ : Satisfies M w₃ q
⊢ Satisfies M w₃ p
Tactic:
exact Satisfies.formula_hereditary hw₂₃ hp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.disj₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ p ⟶ p ⋎ q
Tactic:
simp_all [ValidOnModel]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.disj₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ q ⟶ p ⋎ q
Tactic:
simp_all [ValidOnModel]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.disj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ (p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r
Tactic:
simp_all only [ValidOnModel.iff_models, ValidOnModel, Satisfies.iff_models, Satisfies.imp_def, Satisfies.or_def]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' →
      (∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 p → Satisfies M w'_1 r) →
        ∀ {w'_1 : M.Frame.World},
          w' ≺ w'_1 →
            (∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' q → Satisfies M w' r) →
              ∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' p ∨ Satisfies M w' q → Satisfies M w' r
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.disj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' →
      (∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 p → Satisfies M w'_1 r) →
        ∀ {w'_1 : M.Frame.World},
          w' ≺ w'_1 →
            (∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' q → Satisfies M w' r) →
              ∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' p ∨ Satisfies M w' q → Satisfies M w' r
Tactic:
intro w₁ w₂ _ hpr w₃ hw₂₃ hqr w₄ hw₃₄ hpq
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpr : ∀ {w' : M.Frame.World}, w₂ ≺ w' → Satisfies M w' p → Satisfies M w' r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hqr : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' q → Satisfies M w' r
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hpq : Satisfies M w₄ p ∨ Satisfies M w₄ q
⊢ Satisfies M w₄ r
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.disj₃
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpr : ∀ {w' : M.Frame.World}, w₂ ≺ w' → Satisfies M w' p → Satisfies M w' r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hqr : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' q → Satisfies M w' r
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hpq : Satisfies M w₄ p ∨ Satisfies M w₄ q
⊢ Satisfies M w₄ r
Tactic:
cases hpq with
| inl hp => exact hpr (M.Frame.Rel_trans hw₂₃ hw₃₄) hp;
| inr hq => exact hqr hw₃₄ hq;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.disj₃
Proof state before:
case inl
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpr : ∀ {w' : M.Frame.World}, w₂ ≺ w' → Satisfies M w' p → Satisfies M w' r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hqr : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' q → Satisfies M w' r
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hp : Satisfies M w₄ p
⊢ Satisfies M w₄ r
Tactic:
exact hpr (M.Frame.Rel_trans hw₂₃ hw₃₄) hp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.disj₃
Proof state before:
case inr
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpr : ∀ {w' : M.Frame.World}, w₂ ≺ w' → Satisfies M w' p → Satisfies M w' r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hqr : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' q → Satisfies M w' r
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hq : Satisfies M w₄ q
⊢ Satisfies M w₄ r
Tactic:
exact hqr hw₃₄ hq
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.imply₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ p ⟶ q ⟶ p
Tactic:
simp_all [ValidOnModel]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' → Satisfies M w' p → ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 q → Satisfies M w'_1 p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.imply₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' → Satisfies M w' p → ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 q → Satisfies M w'_1 p
Tactic:
intro w₁ w₂ _ hp w₃ hw₂₃ _
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝¹ : w₁ ≺ w₂
hp : Satisfies M w₂ p
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
a✝ : Satisfies M w₃ q
⊢ Satisfies M w₃ p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.imply₁
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝¹ : w₁ ≺ w₂
hp : Satisfies M w₂ p
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
a✝ : Satisfies M w₃ q
⊢ Satisfies M w₃ p
Tactic:
exact Satisfies.formula_hereditary hw₂₃ hp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.imply₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ (p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r
Tactic:
simp_all only [ValidOnModel.iff_models, ValidOnModel, Satisfies.iff_models, Satisfies.imp_def]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' →
      (∀ {w'_1 : M.Frame.World},
          w' ≺ w'_1 → Satisfies M w'_1 p → ∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' q → Satisfies M w' r) →
        ∀ {w'_1 : M.Frame.World},
          w' ≺ w'_1 →
            (∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' p → Satisfies M w' q) →
              ∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' p → Satisfies M w' r
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.imply₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' →
      (∀ {w'_1 : M.Frame.World},
          w' ≺ w'_1 → Satisfies M w'_1 p → ∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' q → Satisfies M w' r) →
        ∀ {w'_1 : M.Frame.World},
          w' ≺ w'_1 →
            (∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' p → Satisfies M w' q) →
              ∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' p → Satisfies M w' r
Tactic:
intro w₁ w₂ _ hpqr w₃ hw₂₃ hpq w₄ hw₃₄ hp
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpqr :
  ∀ {w' : M.Frame.World},
    w₂ ≺ w' → Satisfies M w' p → ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 q → Satisfies M w'_1 r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hpq : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' p → Satisfies M w' q
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hp : Satisfies M w₄ p
⊢ Satisfies M w₄ r
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.imply₂
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpqr :
  ∀ {w' : M.Frame.World},
    w₂ ≺ w' → Satisfies M w' p → ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 q → Satisfies M w'_1 r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hpq : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' p → Satisfies M w' q
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hp : Satisfies M w₄ p
⊢ Satisfies M w₄ r
Tactic:
exact hpqr (M.Frame.Rel_trans hw₂₃ hw₃₄) hp (M.Frame.Rel_refl w₄) (hpq hw₃₄ hp)
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.mdp
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hpq : M ⊧ p ⟶ q
hp : M ⊧ p
⊢ M ⊧ q
Tactic:
simp_all [ValidOnModel]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hpq : ∀ (w : M.World) {w' : M.Frame.World}, w ≺ w' → Satisfies M w' q
hp : ∀ (w : M.World), Satisfies M w p
⊢ ∀ (w : M.World), Satisfies M w q
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.mdp
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hpq : ∀ (w : M.World) {w' : M.Frame.World}, w ≺ w' → Satisfies M w' q
hp : ∀ (w : M.World), Satisfies M w p
⊢ ∀ (w : M.World), Satisfies M w q
Tactic:
intro w
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hpq : ∀ (w : M.World) {w' : M.Frame.World}, w ≺ w' → Satisfies M w' q
hp : ∀ (w : M.World), Satisfies M w p
w : M.World
⊢ Satisfies M w q
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.mdp
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hpq : ∀ (w : M.World) {w' : M.Frame.World}, w ≺ w' → Satisfies M w' q
hp : ∀ (w : M.World), Satisfies M w p
w : M.World
⊢ Satisfies M w q
Tactic:
exact hpq _ (M.Frame.Rel_refl w)
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.efq
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ Axioms.EFQ p
Tactic:
simp_all [ValidOnModel]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
⊢ M ⊧ Axioms.LEM p
Tactic:
simp_all [ValidOnModel]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
⊢ ∀ (w : M.World), Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
⊢ ∀ (w : M.World), Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
intro w
Proof state after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem
Proof state before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
by_cases h : w ⊧ p
Proof state after:
case pos
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p

case neg
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p