FS000Z · theorem body

four_square_conjugate_mixed_decomposition

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Each of the twelve conjugate same-sign mixed blocks crosses its right factors into its unique opposite-sign correction block.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

forall a b c d e f g h. (((((((((((((((a * e) * (b * f) + (b * f) * (a * e))) + (((a * e) * (c * g) + (c * g) * (a * e)))) + (((b * f) * (c * g) + (c * g) * (b * f)))) + (((d * h) * (a * e) + (a * e) * (d * h)))) + (((d * h) * (b * f) + (b * f) * (d * h)))) + (((d * h) * (c * g) + (c * g) * (d * h)))) + (((a * f) * (c * h) + (c * h) * (a * f)))) + (((b * e) * (d * g) + (d * g) * (b * e)))) + (((a * g) * (d * f) + (d * f) * (a * g)))) + (((c * e) * (b * h) + (b * h) * (c * e)))) + (((a * h) * (b * g) + (b * g) * (a * h)))) + (((d * e) * (c * f) + (c * f) * (d * e))))) = (((((((((((((((a * f) * (b * e) + (b * e) * (a * f))) + (((a * f) * (d * g) + (d * g) * (a * f)))) + (((c * h) * (b * e) + (b * e) * (c * h)))) + (((c * h) * (d * g) + (d * g) * (c * h)))) + (((a * g) * (c * e) + (c * e) * (a * g)))) + (((a * g) * (b * h) + (b * h) * (a * g)))) + (((d * f) * (c * e) + (c * e) * (d * f)))) + (((d * f) * (b * h) + (b * h) * (d * f)))) + (((a * h) * (d * e) + (d * e) * (a * h)))) + (((a * h) * (c * f) + (c * f) * (a * h)))) + (((b * g) * (d * e) + (d * e) * (b * g)))) + (((b * g) * (c * f) + (c * f) * (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

none

In local proof propositions

none
Exact expanded first-order statement
forall a b c d e f g h. (((((((((((((((a * e) * (b * f) + (b * f) * (a * e))) + (((a * e) * (c * g) + (c * g) * (a * e)))) + (((b * f) * (c * g) + (c * g) * (b * f)))) + (((d * h) * (a * e) + (a * e) * (d * h)))) + (((d * h) * (b * f) + (b * f) * (d * h)))) + (((d * h) * (c * g) + (c * g) * (d * h)))) + (((a * f) * (c * h) + (c * h) * (a * f)))) + (((b * e) * (d * g) + (d * g) * (b * e)))) + (((a * g) * (d * f) + (d * f) * (a * g)))) + (((c * e) * (b * h) + (b * h) * (c * e)))) + (((a * h) * (b * g) + (b * g) * (a * h)))) + (((d * e) * (c * f) + (c * f) * (d * e))))) = (((((((((((((((a * f) * (b * e) + (b * e) * (a * f))) + (((a * f) * (d * g) + (d * g) * (a * f)))) + (((c * h) * (b * e) + (b * e) * (c * h)))) + (((c * h) * (d * g) + (d * g) * (c * h)))) + (((a * g) * (c * e) + (c * e) * (a * g)))) + (((a * g) * (b * h) + (b * h) * (a * g)))) + (((d * f) * (c * e) + (c * e) * (d * f)))) + (((d * f) * (b * h) + (b * h) * (d * f)))) + (((a * h) * (d * e) + (d * e) * (a * h)))) + (((a * h) * (c * f) + (c * f) * (a * h)))) + (((b * g) * (d * e) + (d * e) * (b * g)))) + (((b * g) * (c * f) + (c * f) * (b * g)))))

Proof neighborhood

Direct theorem prerequisites

FS002Q four_square_euler_double_cross_swap add_assoc · Stable closed add_comm · Stable closed FS0006 four_square_add_swap_right_tail

Direct theorem dependents

FS0010 four_square_conjugate_global_compensation

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.

Read the argument

Proof checkpoints

178 script commands · 34 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
four square euler double cross swapfour square add swap right tail
01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro f
  7. L7
    intro g
  8. L8
    intro h
02Calculate and transport equalitiesL9–18

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L9
    trans ((((((((((((((a * f) * (b * e) + (b * e) * (a * f))) + (((a * g) * (c * e) + (c * e) * (a * g)))) + (((b * g) * (c * f) + (c * f) * (b * g)))) + (((a * h) * (d * e) + (d * e) * (a * h)))) + (((d * f) * (b * h) + (b * h) * (d * f)))) + (((c * h) * (d * g) + (d * g) * (c * h)))) + (((a * h) * (c * f) + (c * f) * (a * h)))) + (((b * g) * (d * e) + (d * e) * (b * g)))) + (((a * f) * (d * g) + (d * g) * (a * f)))) + (((c * h) * (b * e) + (b * e) * (c * h)))) + (((a * g) * (b * h) + (b * h) * (a * g)))) + (((d * f) * (c * e) + (c * e) * (d * f))))
  2. L10
    congr
  3. L11
    congr
  4. L12
    congr
  5. L13
    congr
  6. L14
    congr
  7. L15
    congr
  8. L16
    congr
  9. L17
    congr
  10. L18
    congr
03Calculate and transport equalitiesL19–20

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L19
    congr
  2. L20
    congr
04Use earlier factsL21–23

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L21
    apply four_square_euler_double_cross_swap
  2. L22
    apply four_square_euler_double_cross_swap
  3. L23
    apply four_square_euler_double_cross_swap
05Calculate and transport equalitiesL24–24

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L24
    trans ((d * e) * (a * h) + (a * h) * (d * e))
06Use earlier factsL25–27

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L25
    apply four_square_euler_double_cross_swap
  2. L26
    apply add_comm
  3. L27
    apply four_square_euler_double_cross_swap
07Calculate and transport equalitiesL28–28

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L28
    trans ((d * g) * (c * h) + (c * h) * (d * g))
08Use earlier factsL29–36

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L29
    apply four_square_euler_double_cross_swap
  2. L30
    apply add_comm
  3. L31
    apply four_square_euler_double_cross_swap
  4. L32
    apply four_square_euler_double_cross_swap
  5. L33
    apply four_square_euler_double_cross_swap
  6. L34
    apply four_square_euler_double_cross_swap
  7. L35
    apply four_square_euler_double_cross_swap
  8. L36
    apply four_square_euler_double_cross_swap
09Calculate and transport equalitiesL37–46

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L37
    trans ((((a * f) * (b * e) + (b * e) * (a * f))) + ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))))))
  2. L38
    simp [add_assoc]
  3. L39
    trans ((((a * f) * (b * e) + (b * e) * (a * f))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((d * f) * (c * e) + (c * e) * (d * f))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((b * g) * (c * f) + (c * f) * (b * g))))))))))))))
  4. L40
    congr
  5. L41
    refl
  6. L42
    trans ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))))
  7. L43
    trans ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))))
  8. L44
    congr
  9. L45
    refl
  10. L46
    trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))))
10Calculate and transport equalitiesL47–56

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L47
    congr
  2. L48
    refl
  3. L49
    trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))
  4. L50
    congr
  5. L51
    refl
  6. L52
    trans ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))
  7. L53
    congr
  8. L54
    refl
  9. L55
    trans ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))
  10. L56
    congr
11Calculate and transport equalitiesL57–60

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L57
    refl
  2. L58
    trans ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))
  3. L59
    congr
  4. L60
    refl
12Use earlier factsL61–67

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L61
    apply four_square_add_swap_right_tail
  2. L62
    apply four_square_add_swap_right_tail
  3. L63
    apply four_square_add_swap_right_tail
  4. L64
    apply four_square_add_swap_right_tail
  5. L65
    apply four_square_add_swap_right_tail
  6. L66
    apply four_square_add_swap_right_tail
  7. L67
    apply four_square_add_swap_right_tail
13Calculate and transport equalitiesL68–77

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L68
    congr
  2. L69
    refl
  3. L70
    trans ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))))
  4. L71
    trans ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))))
  5. L72
    congr
  6. L73
    refl
  7. L74
    trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))
  8. L75
    congr
  9. L76
    refl
  10. L77
    trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))
14Calculate and transport equalitiesL78–87

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L78
    congr
  2. L79
    refl
  3. L80
    trans ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))
  4. L81
    congr
  5. L82
    refl
  6. L83
    trans ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))
  7. L84
    congr
  8. L85
    refl
  9. L86
    trans ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))
  10. L87
    congr
15Calculate and transport equalitiesL88–88

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L88
    refl
16Use earlier factsL89–95

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L89
    apply four_square_add_swap_right_tail
  2. L90
    apply four_square_add_swap_right_tail
  3. L91
    apply four_square_add_swap_right_tail
  4. L92
    apply four_square_add_swap_right_tail
  5. L93
    apply four_square_add_swap_right_tail
  6. L94
    apply four_square_add_swap_right_tail
  7. L95
    apply four_square_add_swap_right_tail
17Calculate and transport equalitiesL96–105

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L96
    congr
  2. L97
    refl
  3. L98
    trans ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))
  4. L99
    trans ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))
  5. L100
    congr
  6. L101
    refl
  7. L102
    trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))
  8. L103
    congr
  9. L104
    refl
  10. L105
    trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))
18Calculate and transport equalitiesL106–107

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L106
    congr
  2. L107
    refl
19Use earlier factsL108–111

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L108
    apply four_square_add_swap_right_tail
  2. L109
    apply four_square_add_swap_right_tail
  3. L110
    apply four_square_add_swap_right_tail
  4. L111
    apply four_square_add_swap_right_tail
20Calculate and transport equalitiesL112–121

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L112
    congr
  2. L113
    refl
  3. L114
    congr
  4. L115
    refl
  5. L116
    trans ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))
  6. L117
    trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))
  7. L118
    congr
  8. L119
    refl
  9. L120
    trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))
  10. L121
    congr
21Calculate and transport equalitiesL122–128

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L122
    refl
  2. L123
    trans ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))
  3. L124
    congr
  4. L125
    refl
  5. L126
    trans ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))
  6. L127
    congr
  7. L128
    refl
22Use earlier factsL129–133

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L129
    apply four_square_add_swap_right_tail
  2. L130
    apply four_square_add_swap_right_tail
  3. L131
    apply four_square_add_swap_right_tail
  4. L132
    apply four_square_add_swap_right_tail
  5. L133
    apply four_square_add_swap_right_tail
23Calculate and transport equalitiesL134–143

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L134
    congr
  2. L135
    refl
  3. L136
    trans ((((d * f) * (c * e) + (c * e) * (d * f))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g))))))))
  4. L137
    trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((d * f) * (c * e) + (c * e) * (d * f))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g))))))))
  5. L138
    congr
  6. L139
    refl
  7. L140
    trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (c * e) + (c * e) * (d * f))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g)))))))
  8. L141
    congr
  9. L142
    refl
  10. L143
    trans ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((d * f) * (c * e) + (c * e) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g))))))
24Calculate and transport equalitiesL144–148

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L144
    congr
  2. L145
    refl
  3. L146
    trans ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((d * f) * (c * e) + (c * e) * (d * f))) + (((b * g) * (d * e) + (d * e) * (b * g)))))
  4. L147
    congr
  5. L148
    refl
25Use earlier factsL149–153

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L149
    apply add_comm
  2. L150
    apply four_square_add_swap_right_tail
  3. L151
    apply four_square_add_swap_right_tail
  4. L152
    apply four_square_add_swap_right_tail
  5. L153
    apply four_square_add_swap_right_tail
26Calculate and transport equalitiesL154–159

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L154
    congr
  2. L155
    refl
  3. L156
    trans ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g)))))))
  4. L157
    trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g)))))))
  5. L158
    congr
  6. L159
    refl
27Use earlier factsL160–161

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L160
    apply four_square_add_swap_right_tail
  2. L161
    apply four_square_add_swap_right_tail
28Calculate and transport equalitiesL162–164

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L162
    congr
  2. L163
    refl
  3. L164
    trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g))))))
29Use earlier factsL165–165

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L165
    apply four_square_add_swap_right_tail
30Calculate and transport equalitiesL166–168

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L166
    congr
  2. L167
    refl
  3. L168
    trans ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + (((b * g) * (d * e) + (d * e) * (b * g)))))
31Use earlier factsL169–169

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L169
    apply four_square_add_swap_right_tail
32Calculate and transport equalitiesL170–172

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L170
    congr
  2. L171
    refl
  3. L172
    trans ((((b * g) * (d * e) + (d * e) * (b * g))) + (((b * g) * (c * f) + (c * f) * (b * g))))
33Use earlier factsL173–173

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L173
    apply add_comm
34Calculate and transport equalitiesL174–178

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L174
    congr
  2. L175
    refl
  3. L176
    refl
  4. L177
    symm
  5. L178
    simp [add_assoc]

Library-wide reading audit

Original defined command ledger · 178 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro h
  9. 0009trans ((((((((((((((a * f) * (b * e) + (b * e) * (a * f))) + (((a * g) * (c * e) + (c * e) * (a * g)))) + (((b * g) * (c * f) + (c * f) * (b * g)))) + (((a * h) * (d * e) + (d * e) * (a * h)))) + (((d * f) * (b * h) + (b * h) * (d * f)))) + (((c * h) * (d * g) + (d * g) * (c * h)))) + (((a * h) * (c * f) + (c * f) * (a * h)))) + (((b * g) * (d * e) + (d * e) * (b * g)))) + (((a * f) * (d * g) + (d * g) * (a * f)))) + (((c * h) * (b * e) + (b * e) * (c * h)))) + (((a * g) * (b * h) + (b * h) * (a * g)))) + (((d * f) * (c * e) + (c * e) * (d * f))))
  10. 0010congr
  11. 0011congr
  12. 0012congr
  13. 0013congr
  14. 0014congr
  15. 0015congr
  16. 0016congr
  17. 0017congr
  18. 0018congr
  19. 0019congr
  20. 0020congr
  21. 0021apply four_square_euler_double_cross_swap
  22. 0022apply four_square_euler_double_cross_swap
  23. 0023apply four_square_euler_double_cross_swap
  24. 0024trans ((d * e) * (a * h) + (a * h) * (d * e))
  25. 0025apply four_square_euler_double_cross_swap
  26. 0026apply add_comm
  27. 0027apply four_square_euler_double_cross_swap
  28. 0028trans ((d * g) * (c * h) + (c * h) * (d * g))
  29. 0029apply four_square_euler_double_cross_swap
  30. 0030apply add_comm
  31. 0031apply four_square_euler_double_cross_swap
  32. 0032apply four_square_euler_double_cross_swap
  33. 0033apply four_square_euler_double_cross_swap
  34. 0034apply four_square_euler_double_cross_swap
  35. 0035apply four_square_euler_double_cross_swap
  36. 0036apply four_square_euler_double_cross_swap
  37. 0037trans ((((a * f) * (b * e) + (b * e) * (a * f))) + ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))))))
  38. 0038simp [add_assoc]
  39. 0039trans ((((a * f) * (b * e) + (b * e) * (a * f))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((d * f) * (c * e) + (c * e) * (d * f))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((b * g) * (c * f) + (c * f) * (b * g))))))))))))))
  40. 0040congr
  41. 0041refl
  42. 0042trans ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))))
  43. 0043trans ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))))
  44. 0044congr
  45. 0045refl
  46. 0046trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))))
  47. 0047congr
  48. 0048refl
  49. 0049trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))
  50. 0050congr
  51. 0051refl
  52. 0052trans ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))
  53. 0053congr
  54. 0054refl
  55. 0055trans ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))
  56. 0056congr
  57. 0057refl
  58. 0058trans ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((a * f) * (d * g) + (d * g) * (a * f))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))
  59. 0059congr
  60. 0060refl
  61. 0061apply four_square_add_swap_right_tail
  62. 0062apply four_square_add_swap_right_tail
  63. 0063apply four_square_add_swap_right_tail
  64. 0064apply four_square_add_swap_right_tail
  65. 0065apply four_square_add_swap_right_tail
  66. 0066apply four_square_add_swap_right_tail
  67. 0067apply four_square_add_swap_right_tail
  68. 0068congr
  69. 0069refl
  70. 0070trans ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))))
  71. 0071trans ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))))
  72. 0072congr
  73. 0073refl
  74. 0074trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))
  75. 0075congr
  76. 0076refl
  77. 0077trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))
  78. 0078congr
  79. 0079refl
  80. 0080trans ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))
  81. 0081congr
  82. 0082refl
  83. 0083trans ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))
  84. 0084congr
  85. 0085refl
  86. 0086trans ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((c * h) * (b * e) + (b * e) * (c * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))
  87. 0087congr
  88. 0088refl
  89. 0089apply four_square_add_swap_right_tail
  90. 0090apply four_square_add_swap_right_tail
  91. 0091apply four_square_add_swap_right_tail
  92. 0092apply four_square_add_swap_right_tail
  93. 0093apply four_square_add_swap_right_tail
  94. 0094apply four_square_add_swap_right_tail
  95. 0095apply four_square_add_swap_right_tail
  96. 0096congr
  97. 0097refl
  98. 0098trans ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))
  99. 0099trans ((((a * g) * (c * e) + (c * e) * (a * g))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))))
  100. 0100congr
  101. 0101refl
  102. 0102trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))))
  103. 0103congr
  104. 0104refl
  105. 0105trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((c * h) * (d * g) + (d * g) * (c * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))
  106. 0106congr
  107. 0107refl
  108. 0108apply four_square_add_swap_right_tail
  109. 0109apply four_square_add_swap_right_tail
  110. 0110apply four_square_add_swap_right_tail
  111. 0111apply four_square_add_swap_right_tail
  112. 0112congr
  113. 0113refl
  114. 0114congr
  115. 0115refl
  116. 0116trans ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))
  117. 0117trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))))
  118. 0118congr
  119. 0119refl
  120. 0120trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))))
  121. 0121congr
  122. 0122refl
  123. 0123trans ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((d * f) * (c * e) + (c * e) * (d * f)))))))
  124. 0124congr
  125. 0125refl
  126. 0126trans ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((a * g) * (b * h) + (b * h) * (a * g))) + ((((b * g) * (d * e) + (d * e) * (b * g))) + (((d * f) * (c * e) + (c * e) * (d * f))))))
  127. 0127congr
  128. 0128refl
  129. 0129apply four_square_add_swap_right_tail
  130. 0130apply four_square_add_swap_right_tail
  131. 0131apply four_square_add_swap_right_tail
  132. 0132apply four_square_add_swap_right_tail
  133. 0133apply four_square_add_swap_right_tail
  134. 0134congr
  135. 0135refl
  136. 0136trans ((((d * f) * (c * e) + (c * e) * (d * f))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g))))))))
  137. 0137trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((d * f) * (c * e) + (c * e) * (d * f))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g))))))))
  138. 0138congr
  139. 0139refl
  140. 0140trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((d * f) * (c * e) + (c * e) * (d * f))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g)))))))
  141. 0141congr
  142. 0142refl
  143. 0143trans ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((d * f) * (c * e) + (c * e) * (d * f))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g))))))
  144. 0144congr
  145. 0145refl
  146. 0146trans ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((d * f) * (c * e) + (c * e) * (d * f))) + (((b * g) * (d * e) + (d * e) * (b * g)))))
  147. 0147congr
  148. 0148refl
  149. 0149apply add_comm
  150. 0150apply four_square_add_swap_right_tail
  151. 0151apply four_square_add_swap_right_tail
  152. 0152apply four_square_add_swap_right_tail
  153. 0153apply four_square_add_swap_right_tail
  154. 0154congr
  155. 0155refl
  156. 0156trans ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g)))))))
  157. 0157trans ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((d * f) * (b * h) + (b * h) * (d * f))) + ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g)))))))
  158. 0158congr
  159. 0159refl
  160. 0160apply four_square_add_swap_right_tail
  161. 0161apply four_square_add_swap_right_tail
  162. 0162congr
  163. 0163refl
  164. 0164trans ((((a * h) * (d * e) + (d * e) * (a * h))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + ((((a * h) * (c * f) + (c * f) * (a * h))) + (((b * g) * (d * e) + (d * e) * (b * g))))))
  165. 0165apply four_square_add_swap_right_tail
  166. 0166congr
  167. 0167refl
  168. 0168trans ((((a * h) * (c * f) + (c * f) * (a * h))) + ((((b * g) * (c * f) + (c * f) * (b * g))) + (((b * g) * (d * e) + (d * e) * (b * g)))))
  169. 0169apply four_square_add_swap_right_tail
  170. 0170congr
  171. 0171refl
  172. 0172trans ((((b * g) * (d * e) + (d * e) * (b * g))) + (((b * g) * (c * f) + (c * f) * (b * g))))
  173. 0173apply add_comm
  174. 0174congr
  175. 0175refl
  176. 0176refl
  177. 0177symm
  178. 0178simp [add_assoc]