How to add a variable?

Stream: new members

[tsuki hao]

Does anyone know how to formalize the informal statement 'The left composition of functions 'f' and 'g' is equal to the composition of the left of 'f' and the left of 'g''.Maybe adding a variable will fix it?

open Complex
theorem comp_left : (f ≫ g).left = f.left ≫ g.left :=by sorry

[Yury G. Kudryashov]

This is not an #mwe

[Yury G. Kudryashov]

What are the types of f and g? What's .left in this context?

[Yury G. Kudryashov]

If you can't prepare a #mwe in Lean, then please write a very detailed markdown/LaTeX statement.

[Yaël Dillies]

I'm not sure what "left composition" is supposed to mean

[Anders Larsson]

I think part of the question is how to prove that function composition is an associative operator.

example: ∀ (f g : ℂ → ℂ ) (x : ℂ), f (g x) = (f ∘ g) x :=  by simp