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

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