Theorem: PropositionalLogic.HilbertSystem.HPM₀.deduction (PropositionalLogic/HilbertSystem/HPM₀.lean)

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ⊢ φ →' ψ) ↔ (Γ ∪ {φ} ⊢ ψ)
Tactic:
apply Iff.intro
State after:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ⊢ φ →' ψ) → (Γ ∪ {φ} ⊢ ψ)

case mpr
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ∪ {φ} ⊢ ψ) → (Γ ⊢ φ →' ψ)

State before:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ⊢ φ →' ψ) → (Γ ∪ {φ} ⊢ ψ)

case mpr
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ∪ {φ} ⊢ ψ) → (Γ ⊢ φ →' ψ)
Tactic:
. intro h;
  have h1 : (Γ ∪ {φ}) ⊢ (φ →' ψ) := weakenContext Γ (Γ ∪ {φ}) (subset_union_left _ _) h;
  have h2 := context (Γ ∪ {φ}) φ (by simp);
  exact MP h1 h2;
State after:
case mpr
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ∪ {φ} ⊢ ψ) → (Γ ⊢ φ →' ψ)

State before:
case mpr
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ∪ {φ} ⊢ ψ) → (Γ ⊢ φ →' ψ)
Tactic:
. admit
State after:
no goals

State before:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ⊢ φ →' ψ) → (Γ ∪ {φ} ⊢ ψ)
Tactic:
intro h
State after:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
⊢ Γ ∪ {φ} ⊢ ψ

State before:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
⊢ Γ ∪ {φ} ⊢ ψ
Tactic:
have h1 : (Γ ∪ {φ}) ⊢ (φ →' ψ) := weakenContext Γ (Γ ∪ {φ}) (subset_union_left _ _) h
State after:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
h1 : Γ ∪ {φ} ⊢ φ →' ψ
⊢ Γ ∪ {φ} ⊢ ψ

State before:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
h1 : Γ ∪ {φ} ⊢ φ →' ψ
⊢ Γ ∪ {φ} ⊢ ψ
Tactic:
have h2 := context (Γ ∪ {φ}) φ (by simp)
State after:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
h1 : Γ ∪ {φ} ⊢ φ →' ψ
h2 : Γ ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ} ⊢ ψ

State before:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
h1 : Γ ∪ {φ} ⊢ φ →' ψ
h2 : Γ ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ} ⊢ ψ
Tactic:
exact MP h1 h2
State after:
no goals

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
h1 : Γ ∪ {φ} ⊢ φ →' ψ
⊢ φ ∈ Γ ∪ {φ}
Tactic:
simp
State after:
no goals

State before:
case mpr
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ∪ {φ} ⊢ ψ) → (Γ ⊢ φ →' ψ)
Tactic:
admit
State after:
no goals