Theorem: PropositionalLogic.HilbertSystem.HPM.distDisj (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 := axiomEConj₁ {φ ∨' ψ ∧' χ} (φ ∧' ψ) χ;
  have h3 := axiomEConj₂ {φ ∨' ψ ∧' χ} (φ ∧' ψ) χ;
  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:
. 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 := axiomEConj₁ {φ ∨' ψ ∧' χ} (φ ∧' ψ) χ
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 := axiomEConj₂ {φ ∨' ψ ∧' χ} (φ ∧' ψ) χ
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:
sorry
State after:
no goals