internlm/Lean-Github huggingface dataset:
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ B ∈ insert A✝ Γ✝, c ⊓ eval v A✝ ≤ eval v B
Tactic:
simp
Proof state after:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ a ∈ Γ✝, c ⊓ eval v A✝ ≤ eval v a
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ a ∈ Γ✝, c ⊓ eval v A✝ ≤ eval v a
Tactic:
intros B hB
Proof state after:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B✝¹ : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
B : Formula
hB : B ∈ Γ✝
⊢ c ⊓ eval v A✝ ≤ eval v B
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B✝¹ : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
B : Formula
hB : B ∈ Γ✝
⊢ c ⊓ eval v A✝ ≤ eval v B
Tactic:
exact inf_le_of_left_le (hv B hB)
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : Γ✝ ⊨ A✝ ⇒ B✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
Tactic:
specialize ih₁ hv
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ≤ eval v (A✝ ⇒ B✝)
⊢ c ≤ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ≤ eval v (A✝ ⇒ B✝)
⊢ c ≤ eval v B✝
Tactic:
simp at ih₁
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ⊓ eval v A✝ ≤ eval v B✝
⊢ c ≤ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ⊓ eval v A✝ ≤ eval v B✝
⊢ c ≤ eval v B✝
Tactic:
rwa [inf_eq_left.mpr (ih₂ hv)] at ih₁
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : Γ✝ ⊨ A✝
ih₂ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ && B✝)
Tactic:
simp [ih₁ hv, ih₂ hv]
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Tactic:
specialize ih hv
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v A✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v A✝
Tactic:
simp at ih
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v A✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v A✝
Tactic:
exact ih.1
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
Tactic:
specialize ih hv
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v B✝
Tactic:
simp at ih
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v B✝
Tactic:
exact ih.2
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
Tactic:
simp
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝
Tactic:
exact le_trans (ih hv) le_sup_left
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
Tactic:
simp
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝
Tactic:
exact le_trans (ih hv) le_sup_right
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₁ : Γ ⊨ A || B
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
⊢ c ≤ eval v C
Tactic:
specialize ih₁ hv
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
⊢ c ≤ eval v C
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
⊢ c ≤ eval v C
Tactic:
have h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D := by
  simp; intros D hD; exact inf_le_of_left_le (hv D hD)
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ c ≤ eval v C
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ c ≤ eval v C
Tactic:
have h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D := by
  simp; intros D hD; exact inf_le_of_left_le (hv D hD)
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ≤ eval v C
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ≤ eval v C
Tactic:
simp at ih₁
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ≤ eval v C
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ≤ eval v C
Tactic:
rw [← inf_eq_left.mpr ih₁, inf_sup_left]
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ⊓ eval v A ⊔ c ⊓ eval v B ≤ eval v C
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ⊓ eval v A ⊔ c ⊓ eval v B ≤ eval v C
Tactic:
rw [← sup_idem (a := eval v C)]
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ⊓ eval v A ⊔ c ⊓ eval v B ≤ eval v C ⊔ eval v C
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ⊓ eval v A ⊔ c ⊓ eval v B ≤ eval v C ⊔ eval v C
Tactic:
exact sup_le_sup (ih₂ h2v) (ih₃ h3v)
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
⊢ ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
Tactic:
simp
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
⊢ ∀ a ∈ Γ, c ⊓ eval v A ≤ eval v a
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
⊢ ∀ a ∈ Γ, c ⊓ eval v A ≤ eval v a
Tactic:
intros D hD
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
D : Formula
hD : D ∈ Γ
⊢ c ⊓ eval v A ≤ eval v D
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
D : Formula
hD : D ∈ Γ
⊢ c ⊓ eval v A ≤ eval v D
Tactic:
exact inf_le_of_left_le (hv D hD)
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
Tactic:
simp
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ ∀ a ∈ Γ, c ⊓ eval v B ≤ eval v a
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ ∀ a ∈ Γ, c ⊓ eval v B ≤ eval v a
Tactic:
intros D hD
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
D : Formula
hD : D ∈ Γ
⊢ c ⊓ eval v B ≤ eval v D
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
D : Formula
hD : D ∈ Γ
⊢ c ⊓ eval v B ≤ eval v D
Tactic:
exact inf_le_of_left_le (hv D hD)
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
ih : Γ✝ ⊨ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Tactic:
specialize ih hv
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v bot
⊢ c ≤ eval v A✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v bot
⊢ c ≤ eval v A✝
Tactic:
simp at ih
Proof state after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c = ⊥
⊢ c ≤ eval v A✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c = ⊥
⊢ c ≤ eval v A✝
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.valid_of_provable
Proof state before:
H : Type ?u.70288
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Provable A
⊢ Valid A
Tactic:
exact soundness_theorem h
Proof state after:
no goals
Theorem: eq_of_abs_sub_le_all
Proof state before:
x y : ℝ
⊢ (∀ ε > 0, |x - y| ≤ ε) → x = y
Tactic:
intro h
Proof state after:
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
⊢ x = y
Theorem: eq_of_abs_sub_le_all
Proof state before:
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
⊢ x = y
Tactic:
apply eq_of_abs_sub_nonpos
Proof state after:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
⊢ |x - y| ≤ 0
Theorem: eq_of_abs_sub_le_all
Proof state before:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
⊢ |x - y| ≤ 0
Tactic:
by_contra H
Proof state after:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : ¬|x - y| ≤ 0
⊢ False
Theorem: eq_of_abs_sub_le_all
Proof state before:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : ¬|x - y| ≤ 0
⊢ False
Tactic:
push_neg at H
Proof state after:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : 0 < |x - y|
⊢ False
Theorem: eq_of_abs_sub_le_all
Proof state before:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : 0 < |x - y|
⊢ False
Tactic:
specialize h (|x-y|/2) (by linarith)
Proof state after:
case h
x y : ℝ
H : 0 < |x - y|
h : |x - y| ≤ |x - y| / 2
⊢ False
Theorem: eq_of_abs_sub_le_all
Proof state before:
case h
x y : ℝ
H : 0 < |x - y|
h : |x - y| ≤ |x - y| / 2
⊢ False
Tactic:
rw [← sub_nonpos, sub_half] at h
Proof state after:
case h
x y : ℝ
H : 0 < |x - y|
h : |x - y| / 2 ≤ 0
⊢ False
Theorem: eq_of_abs_sub_le_all
Proof state before:
case h
x y : ℝ
H : 0 < |x - y|
h : |x - y| / 2 ≤ 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: eq_of_abs_sub_le_all
Proof state before:
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : 0 < |x - y|
⊢ |x - y| / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: abs_sub_le'
Proof state before:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ |a - c| ≤ |a - b| + |c - b|
Tactic:
rw [abs_sub_comm c b]
Proof state after:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ |a - c| ≤ |a - b| + |b - c|