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

State before:
α : Type u_1
⊢ (a : α) → (P Q : dLang α) → δ' (P ⋂ Q) a ≡ (δ' P a ⋂ δ' Q a)
Tactic:
intro a P Q
State after:
α : Type u_1
a : α
P Q : dLang α
⊢ δ' (P ⋂ Q) a ≡ (δ' P a ⋂ δ' Q a)

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

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