`BookProof.ChapterB4.no_pure_state_satisfies_both` : ¬ ∃ ρ, IsPureState ρ ∧ Matrix.trace (ρ * P1) = 1 / 2 ∧ Matrix.trace (ρ * P2) = 1 / 2

Initializing...

`BookProof.ChapterB4.no_pure_state_satisfies_both` : ¬ ∃ ρ, IsPureState ρ ∧ Matrix.trace (ρ * P1) = 1 / 2 ∧ Matrix.trace (ρ * P2) = 1 / 2 · Prove2Me