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

State before:
⊢ y = fun v => structProj v (Sum.inr (Sum.inl ()))
Tactic:
rfl
State after:
no goals