Theorem: PropositionalLogic.HilbertSystem.HPM.distConj (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:
apply ILiff'
State after:
case a
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:
case a
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:
apply And.intro
State after:
case a.left
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
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ

case a.right
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:
case a.left
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
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ

case a.right
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 h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ := by simp;
  have h2 := axiomEDisj {φ ∧' ψ ∨' φ ∧' χ} φ (ψ ∨' χ) ψ;
  have h3 := axiomEDisj {φ ∧' ψ ∨' φ ∧' χ} φ (ψ ∨' χ) χ;
  sorry
State after:
case a.right
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:
case a.right
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 h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ := by simp;
  have h5 := MP (EDisj (axiomEConj₁ _ _ _) (axiomEConj₁ _ _ _)) h1;
  sorry
State after:
no goals

State before:
case a.left
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 h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ := by simp;
State after:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ

State before:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ
Tactic:
have h2 := axiomEDisj {φ ∧' ψ ∨' φ ∧' χ} φ (ψ ∨' χ) ψ
State after:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h2 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' ψ) →' (ψ ∨' χ →' ψ) →' φ ∨' (ψ ∨' χ) →' ψ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ

State before:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h2 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' ψ) →' (ψ ∨' χ →' ψ) →' φ ∨' (ψ ∨' χ) →' ψ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ
Tactic:
have h3 := axiomEDisj {φ ∧' ψ ∨' φ ∧' χ} φ (ψ ∨' χ) χ
State after:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h2 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' ψ) →' (ψ ∨' χ →' ψ) →' φ ∨' (ψ ∨' χ) →' ψ
h3 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' χ) →' (ψ ∨' χ →' χ) →' φ ∨' (ψ ∨' χ) →' χ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ

State before:
case a.left
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h2 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' ψ) →' (ψ ∨' χ →' ψ) →' φ ∨' (ψ ∨' χ) →' ψ
h3 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' χ) →' (ψ ∨' χ →' χ) →' φ ∨' (ψ ∨' χ) →' χ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ
Tactic:
sorry
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:
case a.right
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 h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ := by simp;
State after:
case a.right
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
⊢ ∅ ⊢ φ ∧' ψ ∨' φ ∧' χ →' φ ∧' (ψ ∨' χ)

State before:
case a.right
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
⊢ ∅ ⊢ φ ∧' ψ ∨' φ ∧' χ →' φ ∧' (ψ ∨' χ)
Tactic:
have h5 := MP (EDisj (axiomEConj₁ _ _ _) (axiomEConj₁ _ _ _)) h1
State after:
case a.right
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h5 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ
⊢ ∅ ⊢ φ ∧' ψ ∨' φ ∧' χ →' φ ∧' (ψ ∨' χ)

State before:
case a.right
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
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h5 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ
⊢ ∅ ⊢ φ ∧' ψ ∨' φ ∧' χ →' φ ∧' (ψ ∨' χ)
Tactic:
sorry
State after:
no goals