Hey, guys. It is a second try of my blogging. You know me from my prev. channel and if you don’t know me, it is not a problem, just read my posts. You are here to learn something, not for deanonyming me. Let’s start 😀

Hey. in these days, I started to learn "Lean 4" in parallel while I am learning Haskell. Here my first simple proof you can see:

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  rw [← mul_assoc a b c]
  rw [← mul_assoc b a c]
  rw [mul_comm a b]

In these example, I proved a * (b * c) = b * (a * c) with multiplication association and commutative properties.

1. I rewrite expression on the left with association: a * (b * c) -> a * b *c
2. I rewrite expression on the right with association: b * (a * c) -> b * a * c
3. I rewrite expression on the left with commutative for a and b: a * b * c -> b * a * c
4. Expressions on the left and right now equal with reflexivity: b * a * c = b * a * c