EI002C

eisenstein_product_commute

Genuine Eisenstein multiplication is commutative on represented integer coordinates.

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

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.

A floor quotient in the fundamental parallelogram already gives the required strict norm decrease; global nearest-point optimality is not asserted. The shared carrier is identical to the Gaussian carrier, but the multiplication law and norm are different. Eisenstein gcd, factorization, and prime classification remain separate targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. EisensteinCoordinateProduct(a,b,c,d,e,f,g,h,e · a + f · b + (g · d + h · c),e · b + f · a + (g · c + h · d),e · c + f · d + (g · a + h · b) + (g · d + h · c),e · d + f · c + (g · b + h · a) + (g · c + h · d))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

EisensteinCoordinateProduct(ap,an,bp,bn,cp,cn,dp,dn,rp,rn,sp,sn) · 1

Actual proof prerequisites

add_mul · checked external prerequisitemul_add · checked external prerequisitemul_assoc · checked external prerequisiteadd_assoc · checked external prerequisitemul_comm · checked external prerequisitefour_square_add_swap_right_tail · checked external prerequisite
Original expanded first-order statement 
forall a b c d e f g h. (((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((e) * (b))) + (((f) * (a))))) + (((((g) * (c))) + (((h) * (d)))))))) = ((((((((e) * (a))) + (((f) * (b))))) + (((((g) * (d))) + (((h) * (c))))))) + (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) /\ (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((e) * (d))) + (((f) * (c))))) + (((((g) * (b))) + (((h) * (a))))))) + (((((g) * (c))) + (((h) * (d)))))))) = ((((((((((e) * (c))) + (((f) * (d))))) + (((((g) * (a))) + (((h) * (b))))))) + (((((g) * (d))) + (((h) * (c))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h)))))))))))

Complete tactic proof in conservative notation

All 247 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

247 script commands · 64 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.

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
02Separate the logical casesL9–9

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    split
03Calculate and transport equalitiesL10–19

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

  1. L10
    trans ((((a) * (e))) + ((((b) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((e) * (b))) + ((((f) * (a))) + ((((g) * (c))) + (((h) * (d))))))))))
  2. L11
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  3. L12
    trans ((((a) * (e))) + ((((b) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((b) * (e))) + ((((a) * (f))) + ((((c) * (g))) + (((d) * (h))))))))))
  4. L13
    congr
  5. L14
    refl
  6. L15
    congr
  7. L16
    refl
  8. L17
    congr
  9. L18
    refl
  10. L19
    congr
04Calculate and transport equalitiesL20–22

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

  1. L20
    refl
  2. L21
    congr
  3. L22
    trans ((b) * (e))
05Use earlier factsL23–23

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

  1. L23
    apply mul_comm
06Calculate and transport equalitiesL24–28

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

  1. L24
    congr
  2. L25
    refl
  3. L26
    refl
  4. L27
    congr
  5. L28
    trans ((a) * (f))
07Use earlier factsL29–29

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

  1. L29
    apply mul_comm
08Calculate and transport equalitiesL30–34

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

  1. L30
    congr
  2. L31
    refl
  3. L32
    refl
  4. L33
    congr
  5. L34
    trans ((c) * (g))
09Use earlier factsL35–35

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

  1. L35
    apply mul_comm
10Calculate and transport equalitiesL36–39

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

  1. L36
    congr
  2. L37
    refl
  3. L38
    refl
  4. L39
    trans ((d) * (h))
11Use earlier factsL40–40

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

  1. L40
    apply mul_comm
12Calculate and transport equalitiesL41–49

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

  1. L41
    congr
  2. L42
    refl
  3. L43
    refl
  4. L44
    trans ((((a) * (e))) + ((((b) * (f))) + ((((d) * (g))) + ((((c) * (h))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + (((d) * (h))))))))))
  5. L45
    congr
  6. L46
    refl
  7. L47
    congr
  8. L48
    refl
  9. L49
    trans ((((d) * (g))) + ((((c) * (h))) + ((((b) * (e))) + ((((a) * (f))) + ((((c) * (g))) + (((d) * (h))))))))
13Use earlier factsL50–50

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

  1. L50
    apply four_square_add_swap_right_tail
14Calculate and transport equalitiesL51–55

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

  1. L51
    congr
  2. L52
    refl
  3. L53
    congr
  4. L54
    refl
  5. L55
    trans ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + (((d) * (h))))))
15Use earlier factsL56–56

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

  1. L56
    apply four_square_add_swap_right_tail
16Calculate and transport equalitiesL57–63

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

  1. L57
    congr
  2. L58
    refl
  3. L59
    refl
  4. L60
    trans ((((e) * (a))) + ((((f) * (b))) + ((((g) * (d))) + ((((h) * (c))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + (((d) * (h))))))))))
  5. L61
    symm
  6. L62
    congr
  7. L63
    trans ((a) * (e))
17Use earlier factsL64–64

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

  1. L64
    apply mul_comm
18Calculate and transport equalitiesL65–69

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

  1. L65
    congr
  2. L66
    refl
  3. L67
    refl
  4. L68
    congr
  5. L69
    trans ((b) * (f))
19Use earlier factsL70–70

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

  1. L70
    apply mul_comm
20Calculate and transport equalitiesL71–75

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

  1. L71
    congr
  2. L72
    refl
  3. L73
    refl
  4. L74
    congr
  5. L75
    trans ((d) * (g))
21Use earlier factsL76–76

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

  1. L76
    apply mul_comm
22Calculate and transport equalitiesL77–81

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

  1. L77
    congr
  2. L78
    refl
  3. L79
    refl
  4. L80
    congr
  5. L81
    trans ((c) * (h))
23Use earlier factsL82–82

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

  1. L82
    apply mul_comm
24Calculate and transport equalitiesL83–92

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

  1. L83
    congr
  2. L84
    refl
  3. L85
    refl
  4. L86
    congr
  5. L87
    refl
  6. L88
    congr
  7. L89
    refl
  8. L90
    congr
  9. L91
    refl
  10. L92
    refl
25Calculate and transport equalitiesL93–102

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

  1. L93
    symm
  2. L94
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  3. L95
    trans ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((e) * (d))) + ((((f) * (c))) + ((((g) * (b))) + ((((h) * (a))) + ((((g) * (c))) + (((h) * (d))))))))))))))
  4. L96
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  5. L97
    trans ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h))))))))))))))
  6. L98
    congr
  7. L99
    refl
  8. L100
    congr
  9. L101
    refl
  10. L102
    congr
26Calculate and transport equalitiesL103–111

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

  1. L103
    refl
  2. L104
    congr
  3. L105
    refl
  4. L106
    congr
  5. L107
    refl
  6. L108
    congr
  7. L109
    refl
  8. L110
    congr
  9. L111
    trans ((d) * (e))
27Use earlier factsL112–112

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

  1. L112
    apply mul_comm
28Calculate and transport equalitiesL113–117

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

  1. L113
    congr
  2. L114
    refl
  3. L115
    refl
  4. L116
    congr
  5. L117
    trans ((c) * (f))
29Use earlier factsL118–118

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

  1. L118
    apply mul_comm
30Calculate and transport equalitiesL119–123

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

  1. L119
    congr
  2. L120
    refl
  3. L121
    refl
  4. L122
    congr
  5. L123
    trans ((b) * (g))
31Use earlier factsL124–124

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

  1. L124
    apply mul_comm
32Calculate and transport equalitiesL125–129

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

  1. L125
    congr
  2. L126
    refl
  3. L127
    refl
  4. L128
    congr
  5. L129
    trans ((a) * (h))
33Use earlier factsL130–130

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

  1. L130
    apply mul_comm
34Calculate and transport equalitiesL131–135

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

  1. L131
    congr
  2. L132
    refl
  3. L133
    refl
  4. L134
    congr
  5. L135
    trans ((c) * (g))
35Use earlier factsL136–136

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

  1. L136
    apply mul_comm
36Calculate and transport equalitiesL137–140

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

  1. L137
    congr
  2. L138
    refl
  3. L139
    refl
  4. L140
    trans ((d) * (h))
37Use earlier factsL141–141

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

  1. L141
    apply mul_comm
38Calculate and transport equalitiesL142–149

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

  1. L142
    congr
  2. L143
    refl
  3. L144
    refl
  4. L145
    trans ((((c) * (e))) + ((((d) * (f))) + ((((a) * (g))) + ((((b) * (h))) + ((((d) * (g))) + ((((c) * (h))) + ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + (((d) * (h))))))))))))))
  5. L146
    trans ((((c) * (e))) + ((((a) * (g))) + ((((b) * (h))) + ((((d) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h))))))))))))))
  6. L147
    trans ((((a) * (g))) + ((((c) * (e))) + ((((b) * (h))) + ((((d) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h))))))))))))))
  7. L148
    congr
  8. L149
    refl
39Use earlier factsL150–151

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

  1. L150
    apply four_square_add_swap_right_tail
  2. L151
    apply four_square_add_swap_right_tail
40Calculate and transport equalitiesL152–157

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

  1. L152
    congr
  2. L153
    refl
  3. L154
    trans ((((d) * (f))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h)))))))))))))
  4. L155
    trans ((((a) * (g))) + ((((d) * (f))) + ((((b) * (h))) + ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h)))))))))))))
  5. L156
    congr
  6. L157
    refl
41Use earlier factsL158–159

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

  1. L158
    apply four_square_add_swap_right_tail
  2. L159
    apply four_square_add_swap_right_tail
42Calculate and transport equalitiesL160–166

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

  1. L160
    congr
  2. L161
    refl
  3. L162
    congr
  4. L163
    refl
  5. L164
    congr
  6. L165
    refl
  7. L166
    trans ((((d) * (g))) + ((((c) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h))))))))))
43Use earlier factsL167–167

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

  1. L167
    apply four_square_add_swap_right_tail
44Calculate and transport equalitiesL168–177

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

  1. L168
    congr
  2. L169
    refl
  3. L170
    congr
  4. L171
    refl
  5. L172
    trans ((((a) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((c) * (g))) + (((d) * (h))))))))
  6. L173
    trans ((((d) * (e))) + ((((a) * (h))) + ((((c) * (f))) + ((((b) * (g))) + ((((c) * (g))) + (((d) * (h))))))))
  7. L174
    congr
  8. L175
    refl
  9. L176
    trans ((((c) * (f))) + ((((a) * (h))) + ((((b) * (g))) + ((((c) * (g))) + (((d) * (h)))))))
  10. L177
    congr
45Calculate and transport equalitiesL178–178

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

  1. L178
    refl
46Use earlier factsL179–181

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

  1. L179
    apply four_square_add_swap_right_tail
  2. L180
    apply four_square_add_swap_right_tail
  3. L181
    apply four_square_add_swap_right_tail
47Calculate and transport equalitiesL182–187

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

  1. L182
    congr
  2. L183
    refl
  3. L184
    trans ((((b) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((c) * (g))) + (((d) * (h)))))))
  4. L185
    trans ((((d) * (e))) + ((((b) * (g))) + ((((c) * (f))) + ((((c) * (g))) + (((d) * (h)))))))
  5. L186
    congr
  6. L187
    refl
48Use earlier factsL188–189

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

  1. L188
    apply four_square_add_swap_right_tail
  2. L189
    apply four_square_add_swap_right_tail
49Calculate and transport equalitiesL190–192

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

  1. L190
    congr
  2. L191
    refl
  3. L192
    trans ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + (((d) * (h))))))
50Use earlier factsL193–193

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

  1. L193
    apply four_square_add_swap_right_tail
51Calculate and transport equalitiesL194–200

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

  1. L194
    congr
  2. L195
    refl
  3. L196
    refl
  4. L197
    trans ((((e) * (c))) + ((((f) * (d))) + ((((g) * (a))) + ((((h) * (b))) + ((((g) * (d))) + ((((h) * (c))) + ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + (((d) * (h))))))))))))))
  5. L198
    symm
  6. L199
    congr
  7. L200
    trans ((c) * (e))
52Use earlier factsL201–201

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

  1. L201
    apply mul_comm
53Calculate and transport equalitiesL202–206

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

  1. L202
    congr
  2. L203
    refl
  3. L204
    refl
  4. L205
    congr
  5. L206
    trans ((d) * (f))
54Use earlier factsL207–207

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

  1. L207
    apply mul_comm
55Calculate and transport equalitiesL208–212

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

  1. L208
    congr
  2. L209
    refl
  3. L210
    refl
  4. L211
    congr
  5. L212
    trans ((a) * (g))
56Use earlier factsL213–213

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

  1. L213
    apply mul_comm
57Calculate and transport equalitiesL214–218

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

  1. L214
    congr
  2. L215
    refl
  3. L216
    refl
  4. L217
    congr
  5. L218
    trans ((b) * (h))
58Use earlier factsL219–219

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

  1. L219
    apply mul_comm
59Calculate and transport equalitiesL220–224

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

  1. L220
    congr
  2. L221
    refl
  3. L222
    refl
  4. L223
    congr
  5. L224
    trans ((d) * (g))
60Use earlier factsL225–225

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

  1. L225
    apply mul_comm
61Calculate and transport equalitiesL226–230

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

  1. L226
    congr
  2. L227
    refl
  3. L228
    refl
  4. L229
    congr
  5. L230
    trans ((c) * (h))
62Use earlier factsL231–231

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

  1. L231
    apply mul_comm
63Calculate and transport equalitiesL232–241

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

  1. L232
    congr
  2. L233
    refl
  3. L234
    refl
  4. L235
    congr
  5. L236
    refl
  6. L237
    congr
  7. L238
    refl
  8. L239
    congr
  9. L240
    refl
  10. L241
    congr
64Calculate and transport equalitiesL242–247

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

  1. L242
    refl
  2. L243
    congr
  3. L244
    refl
  4. L245
    refl
  5. L246
    symm
  6. L247
    simp [add_mul, mul_add, mul_assoc, add_assoc]

Library-wide reading audit

Original defined command ledger · 247 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. 0009split
  10. 0010trans ((((a) * (e))) + ((((b) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((e) * (b))) + ((((f) * (a))) + ((((g) * (c))) + (((h) * (d))))))))))
  11. 0011simp [add_mul, mul_add, mul_assoc, add_assoc]
  12. 0012trans ((((a) * (e))) + ((((b) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((b) * (e))) + ((((a) * (f))) + ((((c) * (g))) + (((d) * (h))))))))))
  13. 0013congr
  14. 0014refl
  15. 0015congr
  16. 0016refl
  17. 0017congr
  18. 0018refl
  19. 0019congr
  20. 0020refl
  21. 0021congr
  22. 0022trans ((b) * (e))
  23. 0023apply mul_comm
  24. 0024congr
  25. 0025refl
  26. 0026refl
  27. 0027congr
  28. 0028trans ((a) * (f))
  29. 0029apply mul_comm
  30. 0030congr
  31. 0031refl
  32. 0032refl
  33. 0033congr
  34. 0034trans ((c) * (g))
  35. 0035apply mul_comm
  36. 0036congr
  37. 0037refl
  38. 0038refl
  39. 0039trans ((d) * (h))
  40. 0040apply mul_comm
  41. 0041congr
  42. 0042refl
  43. 0043refl
  44. 0044trans ((((a) * (e))) + ((((b) * (f))) + ((((d) * (g))) + ((((c) * (h))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + (((d) * (h))))))))))
  45. 0045congr
  46. 0046refl
  47. 0047congr
  48. 0048refl
  49. 0049trans ((((d) * (g))) + ((((c) * (h))) + ((((b) * (e))) + ((((a) * (f))) + ((((c) * (g))) + (((d) * (h))))))))
  50. 0050apply four_square_add_swap_right_tail
  51. 0051congr
  52. 0052refl
  53. 0053congr
  54. 0054refl
  55. 0055trans ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + (((d) * (h))))))
  56. 0056apply four_square_add_swap_right_tail
  57. 0057congr
  58. 0058refl
  59. 0059refl
  60. 0060trans ((((e) * (a))) + ((((f) * (b))) + ((((g) * (d))) + ((((h) * (c))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + (((d) * (h))))))))))
  61. 0061symm
  62. 0062congr
  63. 0063trans ((a) * (e))
  64. 0064apply mul_comm
  65. 0065congr
  66. 0066refl
  67. 0067refl
  68. 0068congr
  69. 0069trans ((b) * (f))
  70. 0070apply mul_comm
  71. 0071congr
  72. 0072refl
  73. 0073refl
  74. 0074congr
  75. 0075trans ((d) * (g))
  76. 0076apply mul_comm
  77. 0077congr
  78. 0078refl
  79. 0079refl
  80. 0080congr
  81. 0081trans ((c) * (h))
  82. 0082apply mul_comm
  83. 0083congr
  84. 0084refl
  85. 0085refl
  86. 0086congr
  87. 0087refl
  88. 0088congr
  89. 0089refl
  90. 0090congr
  91. 0091refl
  92. 0092refl
  93. 0093symm
  94. 0094simp [add_mul, mul_add, mul_assoc, add_assoc]
  95. 0095trans ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((e) * (d))) + ((((f) * (c))) + ((((g) * (b))) + ((((h) * (a))) + ((((g) * (c))) + (((h) * (d))))))))))))))
  96. 0096simp [add_mul, mul_add, mul_assoc, add_assoc]
  97. 0097trans ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h))))))))))))))
  98. 0098congr
  99. 0099refl
  100. 0100congr
  101. 0101refl
  102. 0102congr
  103. 0103refl
  104. 0104congr
  105. 0105refl
  106. 0106congr
  107. 0107refl
  108. 0108congr
  109. 0109refl
  110. 0110congr
  111. 0111trans ((d) * (e))
  112. 0112apply mul_comm
  113. 0113congr
  114. 0114refl
  115. 0115refl
  116. 0116congr
  117. 0117trans ((c) * (f))
  118. 0118apply mul_comm
  119. 0119congr
  120. 0120refl
  121. 0121refl
  122. 0122congr
  123. 0123trans ((b) * (g))
  124. 0124apply mul_comm
  125. 0125congr
  126. 0126refl
  127. 0127refl
  128. 0128congr
  129. 0129trans ((a) * (h))
  130. 0130apply mul_comm
  131. 0131congr
  132. 0132refl
  133. 0133refl
  134. 0134congr
  135. 0135trans ((c) * (g))
  136. 0136apply mul_comm
  137. 0137congr
  138. 0138refl
  139. 0139refl
  140. 0140trans ((d) * (h))
  141. 0141apply mul_comm
  142. 0142congr
  143. 0143refl
  144. 0144refl
  145. 0145trans ((((c) * (e))) + ((((d) * (f))) + ((((a) * (g))) + ((((b) * (h))) + ((((d) * (g))) + ((((c) * (h))) + ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + (((d) * (h))))))))))))))
  146. 0146trans ((((c) * (e))) + ((((a) * (g))) + ((((b) * (h))) + ((((d) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h))))))))))))))
  147. 0147trans ((((a) * (g))) + ((((c) * (e))) + ((((b) * (h))) + ((((d) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h))))))))))))))
  148. 0148congr
  149. 0149refl
  150. 0150apply four_square_add_swap_right_tail
  151. 0151apply four_square_add_swap_right_tail
  152. 0152congr
  153. 0153refl
  154. 0154trans ((((d) * (f))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h)))))))))))))
  155. 0155trans ((((a) * (g))) + ((((d) * (f))) + ((((b) * (h))) + ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h)))))))))))))
  156. 0156congr
  157. 0157refl
  158. 0158apply four_square_add_swap_right_tail
  159. 0159apply four_square_add_swap_right_tail
  160. 0160congr
  161. 0161refl
  162. 0162congr
  163. 0163refl
  164. 0164congr
  165. 0165refl
  166. 0166trans ((((d) * (g))) + ((((c) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((a) * (h))) + ((((c) * (g))) + (((d) * (h))))))))))
  167. 0167apply four_square_add_swap_right_tail
  168. 0168congr
  169. 0169refl
  170. 0170congr
  171. 0171refl
  172. 0172trans ((((a) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((b) * (g))) + ((((c) * (g))) + (((d) * (h))))))))
  173. 0173trans ((((d) * (e))) + ((((a) * (h))) + ((((c) * (f))) + ((((b) * (g))) + ((((c) * (g))) + (((d) * (h))))))))
  174. 0174congr
  175. 0175refl
  176. 0176trans ((((c) * (f))) + ((((a) * (h))) + ((((b) * (g))) + ((((c) * (g))) + (((d) * (h)))))))
  177. 0177congr
  178. 0178refl
  179. 0179apply four_square_add_swap_right_tail
  180. 0180apply four_square_add_swap_right_tail
  181. 0181apply four_square_add_swap_right_tail
  182. 0182congr
  183. 0183refl
  184. 0184trans ((((b) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((c) * (g))) + (((d) * (h)))))))
  185. 0185trans ((((d) * (e))) + ((((b) * (g))) + ((((c) * (f))) + ((((c) * (g))) + (((d) * (h)))))))
  186. 0186congr
  187. 0187refl
  188. 0188apply four_square_add_swap_right_tail
  189. 0189apply four_square_add_swap_right_tail
  190. 0190congr
  191. 0191refl
  192. 0192trans ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + (((d) * (h))))))
  193. 0193apply four_square_add_swap_right_tail
  194. 0194congr
  195. 0195refl
  196. 0196refl
  197. 0197trans ((((e) * (c))) + ((((f) * (d))) + ((((g) * (a))) + ((((h) * (b))) + ((((g) * (d))) + ((((h) * (c))) + ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + (((d) * (h))))))))))))))
  198. 0198symm
  199. 0199congr
  200. 0200trans ((c) * (e))
  201. 0201apply mul_comm
  202. 0202congr
  203. 0203refl
  204. 0204refl
  205. 0205congr
  206. 0206trans ((d) * (f))
  207. 0207apply mul_comm
  208. 0208congr
  209. 0209refl
  210. 0210refl
  211. 0211congr
  212. 0212trans ((a) * (g))
  213. 0213apply mul_comm
  214. 0214congr
  215. 0215refl
  216. 0216refl
  217. 0217congr
  218. 0218trans ((b) * (h))
  219. 0219apply mul_comm
  220. 0220congr
  221. 0221refl
  222. 0222refl
  223. 0223congr
  224. 0224trans ((d) * (g))
  225. 0225apply mul_comm
  226. 0226congr
  227. 0227refl
  228. 0228refl
  229. 0229congr
  230. 0230trans ((c) * (h))
  231. 0231apply mul_comm
  232. 0232congr
  233. 0233refl
  234. 0234refl
  235. 0235congr
  236. 0236refl
  237. 0237congr
  238. 0238refl
  239. 0239congr
  240. 0240refl
  241. 0241congr
  242. 0242refl
  243. 0243congr
  244. 0244refl
  245. 0245refl
  246. 0246symm
  247. 0247simp [add_mul, mul_add, mul_assoc, add_assoc]