Theorem: PropositionalLogic.HilbertSystem.HPM.ELiff_mpr' (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
Γ : Finset 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
Γ : Finset 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
Γ : Finset L
φ₁ φ₂ : L
⊢ (Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)) → (Γ ∪ {φ₂} ⊢ φ₁)
Tactic:
intro h
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ∪ {φ₂} ⊢ φ₁

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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ∪ {φ₂} ⊢ φ₁
Tactic:
have s1 : Γ ∪ {φ₂} ⊢ φ₂ := 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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₂} ⊢ φ₂
s2 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₂ →' φ₁
⊢ Γ ∪ {φ₂} ⊢ φ₁
Tactic:
have s3 := weakenContext Γ (Γ ∪ {φ₂}) (by simp) h
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₂} ⊢ φ₂
s2 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₂ →' φ₁
s3 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ∪ {φ₂} ⊢ φ₁
Tactic:
have s4 := MP s2 s3
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₂} ⊢ φ₂
s2 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₂ →' φ₁
s3 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s4 : Γ ∪ {φ₂} ⊢ φ₂ →' φ₁
⊢ Γ ∪ {φ₂} ⊢ φ₁
Tactic:
have s5 := MP s4 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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₂} ⊢ φ₂
s2 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₂ →' φ₁
s3 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s4 : Γ ∪ {φ₂} ⊢ φ₂ →' φ₁
s5 : Γ ∪ {φ₂} ⊢ φ₁
⊢ Γ ∪ {φ₂} ⊢ φ₁
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
⊢ Γ ∪ {φ₂} ⊢ φ₂
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
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
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁)
s1 : Γ ∪ {φ₂} ⊢ φ₂
s2 : Γ ∪ {φ₂} ⊢ (φ₁ →' φ₂) ∧' (φ₂ →' φ₁) →' φ₂ →' φ₁
⊢ Γ ⊆ Γ ∪ {φ₂}
Tactic:
simp
State after:
no goals