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

State before:
α : Type u_1
⊢ (a c : α) → δ' (char c) a ≡ (a ≡ c · ε)
Tactic:
intros a c
State after:
α : Type u_1
a c : α
⊢ δ' (char c) a ≡ (a ≡ c · ε)

State before:
α : Type u_1
a c : α
⊢ δ' (char c) a ≡ (a ≡ c · ε)
Tactic:
unfold δ'
State after:
α : Type u_1
a c : α
⊢ (fun w => char c (a :: w)) ≡ (a ≡ c · ε)

State before:
α : Type u_1
a c : α
⊢ (fun w => char c (a :: w)) ≡ (a ≡ c · ε)
Tactic:
unfold char
State after:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ (a ≡ c · ε)

State before:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ (a ≡ c · ε)
Tactic:
unfold emptyStr
State after:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ (a ≡ c · fun w => w ≡ [])

State before:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ (a ≡ c · fun w => w ≡ [])
Tactic:
unfold scalar
State after:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ fun w => a ≡ c × (fun w => w ≡ []) w

State before:
α : Type u_1
a c : α
⊢ (fun w => a :: w ≡ [c]) ≡ fun w => a ≡ c × (fun w => w ≡ []) w
Tactic:
sorry
State after:
no goals