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

State before:
a b : Point
⊢ addAlt a b = addAlt b a
Tactic:
rw [addAlt, addAlt]
State after:
a b : Point
⊢ (match a, b with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }) =
    match b, a with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }

State before:
a b : Point
⊢ (match a, b with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }) =
    match b, a with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + 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