Theorem: Float3.z.as_struct_modify (test/deriving/structure_ops.lean)

State before:
f : Float → Float
v : Float3
⊢ { x := v.x, y := v.y, z := f v.z } = structModify (Sum.inr (Sum.inr ())) f v
Tactic:
rfl
State after:
no goals