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

State before:
α : Type
⊢ (a : α) → (s : Type) → (P : dLang α) → δ (s · P) a ≡ (s · δ' P a)
Tactic:
intro a s P
State after:
α : Type
a : α
s : Type
P : dLang α
⊢ δ (s · P) a ≡ (s · δ' P a)

State before:
α : Type
a : α
s : Type
P : dLang α
⊢ δ (s · P) a ≡ (s · δ' P a)
Tactic:
constructor
State after:
case a
α : Type
a : α
s : Type
P : dLang α
⊢ δ (s · P) a = (s · δ' P a)

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