Theorem: C06S01.Point.add_comm (MIL/C06_Structures/S01_Structures.lean)

State before:
a b : Point
⊢ a.add b = b.add a
Tactic:
rw [add, add]
State after:
a b : Point
⊢ { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z } = { x := b.x + a.x, y := b.y + a.y, z := b.z + a.z }

State before:
a b : Point
⊢ { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z } = { x := b.x + a.x, y := b.y + a.y, z := b.z + a.z }
Tactic:
ext <;> dsimp
State after:
case x
a b : Point
⊢ a.x + b.x = b.x + a.x

case y
a b : Point
⊢ a.y + b.y = b.y + a.y

case z
a b : Point
⊢ a.z + b.z = b.z + a.z

State before:
case x
a b : Point
⊢ a.x + b.x = b.x + a.x

case y
a b : Point
⊢ a.y + b.y = b.y + a.y

case z
a b : Point
⊢ a.z + b.z = b.z + a.z
Tactic:
repeat' apply add_comm
State after:
no goals

State before:
case z
a b : Point
⊢ a.z + b.z = b.z + a.z
Tactic:
apply add_comm
State after:
no goals