internlm/Lean-Github huggingface dataset:
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
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.104354
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.104354
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
Proof state after:
case h2v
H✝ : Type ?u.104354
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

H✝ : Type ?u.104354
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.104354
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
Proof state after:
case h3v
H✝ : Type ?u.104354
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

H✝ : Type ?u.104354
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.104354
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.104354
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.104354
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.104354
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.104354
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.104354
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.104354
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:
case h2v
H✝ : Type ?u.104354
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:
case h2v
H✝ : Type ?u.104354
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:
case h2v
H✝ : Type ?u.104354
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:
case h2v
H✝ : Type ?u.104354
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:
case h2v
H✝ : Type ?u.104354
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:
case h3v
H✝ : Type ?u.104354
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:
case h3v
H✝ : Type ?u.104354
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:
case h3v
H✝ : Type ?u.104354
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:
case h3v
H✝ : Type ?u.104354
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:
case h3v
H✝ : Type ?u.104354
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.104354
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.104354
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.104354
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.104354
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.104354
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.129241
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: IntuitionisticPropositionalLogic.eval_top
Proof state before:
H : Type u_1
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
⊢ eval v top = ⊤
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.isTrue_equiv
Proof state before:
H : Type u_1
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
⊢ eval v (A ⇔ B) = (eval v A ⇨ eval v B) ⊓ (eval v B ⇨ eval v A)
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.87019
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
h2 : Γ ⊆ Δ
⊢ Δ ⊢ A
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.ProvableFrom.insert
Proof state before:
H : Type ?u.87077
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Insert.insert B Γ ⊢ A
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.deduction_theorem
Proof state before:
H : Type ?u.87138
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ B
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.Provable.mp
Proof state before:
H : Type ?u.87199
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ B
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H : Type ?u.87239
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊨ A
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.valid_of_provable
Proof state before:
H : Type ?u.87275
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Provable A
⊢ Valid A
Tactic:
sorry
Proof state after:
no goals
Theorem: uniq_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
⊢ seq_limit u l → seq_limit u l' → l = l'
Tactic:
intros hl hl'
Proof state after:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ l = l'
Theorem: uniq_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ l = l'
Tactic:
apply eq_of_abs_sub_le_all
Proof state after:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ ∀ ε > 0, |l - l'| ≤ ε
Theorem: uniq_limit
Proof state before:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ ∀ ε > 0, |l - l'| ≤ ε
Tactic:
intros ε ε_pos
Proof state after:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ |l - l'| ≤ ε
Theorem: uniq_limit
Proof state before:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ |l - l'| ≤ ε
Tactic:
rcases hl (ε/2) (by linarith) with ⟨N, hN⟩
Proof state after:
case a.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: uniq_limit
Proof state before:
case a.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
rcases hl' (ε/2) (by linarith) with ⟨N', hN'⟩
Proof state after:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: uniq_limit
Proof state before:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
calc
  |l - l'| ≤ |l - u (max N N')| + |u (max N N') - l'| := by apply abs_sub_le
         _ = |u (max N N') - l| + |u (max N N') - l'| := by rw [abs_sub_comm]
         _ ≤ ε := by linarith [hN _ (le_max_left N N'), hN' _ (le_max_right N N')]
Proof state after:
no goals
Theorem: uniq_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ ε / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: uniq_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ ε / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: uniq_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ |l - u (max N N')| + |u (max N N') - l'|
Tactic:
apply abs_sub_le
Proof state after:
no goals
Theorem: uniq_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - u (max N N')| + |u (max N N') - l'| = |u (max N N') - l| + |u (max N N') - l'|
Tactic:
rw [abs_sub_comm]
Proof state after:
no goals
Theorem: uniq_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |u (max N N') - l| + |u (max N N') - l'| ≤ ε
Tactic:
linarith [hN _ (le_max_left N N'), hN' _ (le_max_right N N')]
Proof state after:
no goals
Theorem: extraction_ge
Proof state before:
φ : ℕ → ℕ
⊢ extraction φ → ∀ (N N' : ℕ), ∃ n ≥ N', φ n ≥ N
Tactic:
intro h N N'
Proof state after:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ ∃ n ≥ N', φ n ≥ N
Theorem: extraction_ge
Proof state before:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ ∃ n ≥ N', φ n ≥ N
Tactic:
use max N N'
Proof state after:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N' ∧ φ (max N N') ≥ N
Theorem: extraction_ge
Proof state before:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N' ∧ φ (max N N') ≥ N
Tactic:
constructor
Proof state after:
case left
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N'

case right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
Theorem: extraction_ge
Proof state before:
case left
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N'

case right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
Tactic:
apply le_max_right
Proof state after:
case right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
Theorem: extraction_ge
Proof state before:
case right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
Tactic:
calc
  N ≤ max N N' := by apply le_max_left
  _ ≤ φ (max N N') := by apply id_le_extraction' h
Proof state after:
no goals
Theorem: extraction_ge
Proof state before:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ N ≤ max N N'
Tactic:
apply le_max_left
Proof state after:
no goals
Theorem: extraction_ge
Proof state before:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≤ φ (max N N')
Tactic:
apply id_le_extraction' h
Proof state after:
no goals
Theorem: near_cluster
Proof state before:
u : ℕ → ℝ
a : ℝ
⊢ cluster_point u a → ∀ ε > 0, ∀ (N : ℕ), ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
intro hyp ε ε_pos N
Proof state after:
u : ℕ → ℝ
a : ℝ
hyp : cluster_point u a
ε : ℝ
ε_pos : ε > 0
N : ℕ
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Theorem: near_cluster
Proof state before:
u : ℕ → ℝ
a : ℝ
hyp : cluster_point u a
ε : ℝ
ε_pos : ε > 0
N : ℕ
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
rcases hyp with ⟨φ, φ_extr, hφ⟩
Proof state after:
case intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Theorem: near_cluster
Proof state before:
case intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
cases' hφ ε ε_pos with N' hN'
Proof state after:
case intro.intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
N' : ℕ
hN' : ∀ n ≥ N', |(u ∘ φ) n - a| ≤ ε
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Theorem: near_cluster
Proof state before:
case intro.intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
N' : ℕ
hN' : ∀ n ≥ N', |(u ∘ φ) n - a| ≤ ε
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
rcases extraction_ge φ_extr N N' with ⟨q, hq, hq'⟩
Proof state after:
case intro.intro.intro.intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
N' : ℕ
hN' : ∀ n ≥ N', |(u ∘ φ) n - a| ≤ ε
q : ℕ
hq : q ≥ N'
hq' : φ q ≥ N
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Theorem: near_cluster
Proof state before:
case intro.intro.intro.intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
N' : ℕ
hN' : ∀ n ≥ N', |(u ∘ φ) n - a| ≤ ε
q : ℕ
hq : q ≥ N'
hq' : φ q ≥ N
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
exact ⟨φ q, hq', hN' _ hq⟩
Proof state after:
no goals
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
⊢ seq_limit (u ∘ φ) l
Tactic:
intro ε ε_pos
Proof state after:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Tactic:
cases' h ε ε_pos with N hN
Proof state after:
case intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
case intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Tactic:
use N
Proof state after:
case intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
case intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Tactic:
intro n hn
Proof state after:
case intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - l| ≤ ε