Theorem: Float3.mk.as_struct_make (test/deriving/structure_ops.lean)

State before:
f : (i : Unit ⊕ Unit ⊕ Unit) → Sum.rec (fun x => Float) (fun t => Sum.rec (fun x => Float) (fun x => Float) t) i
⊢ { x := f (Sum.inl ()), y := f (Sum.inr (Sum.inl ())), z := f (Sum.inr (Sum.inr ())) } = structMake f
Tactic:
rfl
State after:
no goals