Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁ (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:
simp [deduction]
State after:
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:
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:
have s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ := by simp;
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'

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
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ := by simp;
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'

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
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥' := by simp;
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'

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
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s4 := MP s2 s1
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'

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
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s5 := MP s3 s4
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ
s5 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'

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
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ
s5 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
assumption
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
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
Tactic:
simp
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
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
Tactic:
simp
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
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
Tactic:
simp
State after:
no goals