theorem TLA.ProofMode.Entails_and_split {σ : Type u} {hyps : List (NamedPred σ)} {g1 g2 : pred σ} : Entails hyps [tlafml|g1 ∧ g2] = (Entails hyps g1 ∧ Entails hyps g2)

def TLA.ProofMode.tacticTlaSplitAnds : Lean.ParserDescr

tlaSplitAnds splits a conjunctive proof-mode goal into separate goals.

For example, if the proof-mode goal is p ∧ q, then

tlaSplitAnds

creates one goal for p and one goal for q.

Equations

• TLA.ProofMode.tacticTlaSplitAnds = Lean.ParserDescr.node `TLA.ProofMode.tacticTlaSplitAnds 1024 (Lean.ParserDescr.nonReservedSymbol "tlaSplitAnds" false)