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

State before:
⊢ HasSemiAdjoint Float fun v => v.x
Tactic:
rw[Float3.x.as_struct_proj]
State after:
⊢ HasSemiAdjoint Float fun v => (fun v => structProj v (Sum.inl ())) v

State before:
⊢ HasSemiAdjoint Float fun v => (fun v => structProj v (Sum.inl ())) v
Tactic:
sorry_proof
State after:
no goals