Theorem: nullable_and (Katydid/Conal/Calculus.lean)

State before:
α : Type (max u_1 u_2)
⊢ (P Q : dLang α) → ν' (P ⋂ Q) ≡ (ν' P × ν' Q)
Tactic:
intro P Q
State after:
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋂ Q) ≡ (ν' P × ν' Q)

State before:
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋂ Q) ≡ (ν' P × ν' Q)
Tactic:
constructor
State after:
case a
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋂ Q) = (ν' P × ν' Q)

State before:
case a
α : Type (max u_1 u_2)
P Q : dLang α
⊢ ν' (P ⋂ Q) = (ν' P × ν' Q)
Tactic:
rfl
State after:
no goals