0f7fb1ea4d
This PR adds general projection lemmas for `ExceptConds` conjunction: - `ExceptConds.and_elim_left`: `(x ∧ₑ y) ⊢ₑ x` - `ExceptConds.and_elim_right`: `(x ∧ₑ y) ⊢ₑ y` The existing `and_true`, `true_and`, `and_false`, `false_and` are refactored as one-line corollaries. Suggested by @sgraf812 in https://github.com/leanprover-community/cslib/pull/376#discussion_r2066993469. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| Data | ||
| Do | ||
| Internal | ||
| Net | ||
| Sat | ||
| Sync | ||
| Tactic | ||
| Time | ||
| Data.lean | ||
| Do.lean | ||
| Internal.lean | ||
| Net.lean | ||
| Sat.lean | ||
| Sync.lean | ||
| Tactic.lean | ||
| Time.lean | ||