four_square_conjugate_coordinate_square_transport

Statement with defined notation

forall a b c d e f g h m0 m1 m2 m3. ((((a * e + b * f + c * g + d * h) = (0) + m0) \/ ((0) = (a * e + b * f + c * g + d * h) + m0)) /\ ((((a * f + c * h) = (b * e + d * g) + m1) \/ ((b * e + d * g) = (a * f + c * h) + m1)) /\ ((((a * g + d * f) = (c * e + b * h) + m2) \/ ((c * e + b * h) = (a * g + d * f) + m2)) /\ (((a * h + b * g) = (d * e + c * f) + m3) \/ ((d * e + c * f) = (a * h + b * g) + m3))))) -> ((((a * e + b * f + c * g + d * h) * (a * e + b * f + c * g + d * h) + (0) * (0)) = (((m0) * (m0)) + ((a * e + b * f + c * g + d * h) * (0) + (0) * (a * e + b * f + c * g + d * h)))) /\ ((((a * f + c * h) * (a * f + c * h) + (b * e + d * g) * (b * e + d * g)) = (((m1) * (m1)) + ((a * f + c * h) * (b * e + d * g) + (b * e + d * g) * (a * f + c * h)))) /\ ((((a * g + d * f) * (a * g + d * f) + (c * e + b * h) * (c * e + b * h)) = (((m2) * (m2)) + ((a * g + d * f) * (c * e + b * h) + (c * e + b * h) * (a * g + d * f)))) /\ (((a * h + b * g) * (a * h + b * g) + (d * e + c * f) * (d * e + c * f)) = (((m3) * (m3)) + ((a * h + b * g) * (d * e + c * f) + (d * e + c * f) * (a * h + b * g)))))))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

In local proof propositions

Proof neighborhood

Direct theorem prerequisites

Direct theorem dependents

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.