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

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