Theorem: PropositionalLogic.HilbertSystem.HPM.lnc (PropositionalLogic/HilbertSystem/HPM.lean)

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
⊢ ∅ ⊢ ¬'(φ ∧' ¬'φ)
Tactic:
simp [deduction]
State after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') := context _ _ (by simp)
State after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s2 : {φ ∧' (φ →' ⊥')} ⊢ (φ ∧' (φ →' ⊥') →' φ) := by apply axiomEConj₁;
State after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s3 : {φ ∧' (φ →' ⊥')} ⊢ (φ ∧' (φ →' ⊥') →' (φ →' ⊥')) := by apply axiomEConj₂;
State after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s4 := MP s2 s1
State after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s5 := MP s3 s1
State after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
s5 : {φ ∧' (φ →' ⊥')} ⊢ φ →' ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
s5 : {φ ∧' (φ →' ⊥')} ⊢ φ →' ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
have s6 := MP s5 s4
State after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
s5 : {φ ∧' (φ →' ⊥')} ⊢ φ →' ⊥'
s6 : {φ ∧' (φ →' ⊥')} ⊢ ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
s3 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
s4 : {φ ∧' (φ →' ⊥')} ⊢ φ
s5 : {φ ∧' (φ →' ⊥')} ⊢ φ →' ⊥'
s6 : {φ ∧' (φ →' ⊥')} ⊢ ⊥'
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'
Tactic:
assumption
State after:
no goals

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
⊢ φ ∧' (φ →' ⊥') ∈ {φ ∧' (φ →' ⊥')}
Tactic:
simp
State after:
no goals

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
⊢ {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
Tactic:
apply axiomEConj₁
State after:
no goals

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
s1 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥')
s2 : {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ
⊢ {φ ∧' (φ →' ⊥')} ⊢ φ ∧' (φ →' ⊥') →' φ →' ⊥'
Tactic:
apply axiomEConj₂
State after:
no goals