EI0028

eisenstein_conjugate_product_is_norm

The actual product of an Eisenstein integer with its genuine conjugate is its natural norm plus zero times ω.

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. ∀ N. EisensteinCoordinateNorm(a,b,c,d,N) → EisensteinCoordinateProduct(a + d,b + c,d,c,a,b,c,d,N,0,0,0)

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

Definition DAG

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

Actual proof prerequisites

eisenstein_pair_natural_value_transportadd_mul · checked external prerequisitemul_add · checked external prerequisitemul_assoc · checked external prerequisiteadd_assoc · checked external prerequisiteadd_comm · checked external prerequisitemul_comm · checked external prerequisitefour_square_add_swap_right_tail · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall a b c d N. (((((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))) + (((((a) * (d))) + (((b) * (c)))))) = ((((((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))) + (((((a) * (c))) + (((b) * (d))))))) + (N))) -> (((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) + (0)) = ((N) + (((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))))) /\ (((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) + (0)) = ((0) + (((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d)))))))))))

Complete tactic proof in conservative notation

All 307 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

307 script commands · 72 reading checkpoints · 1 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 (1)
eisenstein pair natural value transport
01Fix variables and assumptionsL1–6

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 N
  6. L6
    intro hnorm
02Establish hrealL7–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein pair natural value transport.

  1. L7
    have hreal : ((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c)))))) = ((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) + (N))
  2. L8
    specialize eisenstein_pair_natural_value_transport ((((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))) + (((((a) * (d))) + (((b) * (c))))))
  3. L9
    specialize eisenstein_pair_natural_value_transport ((((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))) + (((((a) * (c))) + (((b) * (d))))))
  4. L10
    specialize eisenstein_pair_natural_value_transport ((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
  5. L11
    specialize eisenstein_pair_natural_value_transport ((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))
  6. L12
    specialize eisenstein_pair_natural_value_transport N
  7. L13
    apply eisenstein_pair_natural_value_transport
  8. L14
    exact hnorm
  9. L15
    trans ((((a) * (a))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((d) * (b))) + ((((b) * (a))) + ((((c) * (a))) + ((((d) * (c))) + (((c) * (d))))))))))))))
  10. L16
    simp [add_mul, mul_add, mul_assoc, add_assoc]
03Calculate and transport equalitiesL17–26

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

  1. L17
    trans ((((a) * (a))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))))))))))
  2. L18
    congr
  3. L19
    refl
  4. L20
    congr
  5. L21
    refl
  6. L22
    congr
  7. L23
    refl
  8. L24
    congr
  9. L25
    refl
  10. L26
    congr
04Calculate and transport equalitiesL27–33

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

  1. L27
    refl
  2. L28
    congr
  3. L29
    refl
  4. L30
    congr
  5. L31
    refl
  6. L32
    congr
  7. L33
    trans ((b) * (d))
05Use earlier factsL34–34

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

  1. L34
    apply mul_comm
06Calculate and transport equalitiesL35–39

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

  1. L35
    congr
  2. L36
    refl
  3. L37
    refl
  4. L38
    congr
  5. L39
    trans ((a) * (b))
07Use earlier factsL40–40

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

  1. L40
    apply mul_comm
08Calculate and transport equalitiesL41–45

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
    congr
  5. L45
    trans ((a) * (c))
09Use earlier factsL46–46

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

  1. L46
    apply mul_comm
10Calculate and transport equalitiesL47–51

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
    refl
  4. L50
    congr
  5. L51
    trans ((c) * (d))
11Use earlier factsL52–52

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

  1. L52
    apply mul_comm
12Calculate and transport equalitiesL53–62

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

  1. L53
    congr
  2. L54
    refl
  3. L55
    refl
  4. L56
    refl
  5. L57
    trans ((((a) * (a))) + ((((a) * (d))) + ((((b) * (b))) + ((((b) * (c))) + ((((d) * (d))) + ((((c) * (c))) + ((((a) * (b))) + ((((a) * (b))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (c))) + (((b) * (d))))))))))))))
  6. L58
    congr
  7. L59
    refl
  8. L60
    trans ((((a) * (d))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))))))
  9. L61
    trans ((((b) * (b))) + ((((a) * (d))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))))))
  10. L62
    congr
13Calculate and transport equalitiesL63–66

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

  1. L63
    refl
  2. L64
    trans ((((c) * (c))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))))))))
  3. L65
    congr
  4. L66
    refl
14Use earlier factsL67–69

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

  1. L67
    apply four_square_add_swap_right_tail
  2. L68
    apply four_square_add_swap_right_tail
  3. L69
    apply four_square_add_swap_right_tail
15Calculate and transport equalitiesL70–77

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

  1. L70
    congr
  2. L71
    refl
  3. L72
    congr
  4. L73
    refl
  5. L74
    trans ((((b) * (c))) + ((((c) * (c))) + ((((d) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))))
  6. L75
    trans ((((c) * (c))) + ((((b) * (c))) + ((((d) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))))
  7. L76
    congr
  8. L77
    refl
16Use earlier factsL78–79

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

  1. L78
    apply four_square_add_swap_right_tail
  2. L79
    apply four_square_add_swap_right_tail
17Calculate and transport equalitiesL80–82

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

  1. L80
    congr
  2. L81
    refl
  3. L82
    trans ((((d) * (d))) + ((((c) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))))))
18Use earlier factsL83–83

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

  1. L83
    apply four_square_add_swap_right_tail
19Calculate and transport equalitiesL84–90

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

  1. L84
    congr
  2. L85
    refl
  3. L86
    congr
  4. L87
    refl
  5. L88
    congr
  6. L89
    refl
  7. L90
    trans ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))
20Use earlier factsL91–91

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

  1. L91
    apply four_square_add_swap_right_tail
21Calculate and transport equalitiesL92–97

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

  1. L92
    congr
  2. L93
    refl
  3. L94
    trans ((((c) * (d))) + ((((b) * (d))) + ((((a) * (c))) + (((c) * (d))))))
  4. L95
    trans ((((b) * (d))) + ((((c) * (d))) + ((((a) * (c))) + (((c) * (d))))))
  5. L96
    congr
  6. L97
    refl
22Use earlier factsL98–99

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

  1. L98
    apply four_square_add_swap_right_tail
  2. L99
    apply four_square_add_swap_right_tail
23Calculate and transport equalitiesL100–105

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

  1. L100
    congr
  2. L101
    refl
  3. L102
    trans ((((c) * (d))) + ((((b) * (d))) + (((a) * (c)))))
  4. L103
    trans ((((b) * (d))) + ((((c) * (d))) + (((a) * (c)))))
  5. L104
    congr
  6. L105
    refl
24Use earlier factsL106–107

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

  1. L106
    apply add_comm
  2. L107
    apply four_square_add_swap_right_tail
25Calculate and transport equalitiesL108–110

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

  1. L108
    congr
  2. L109
    refl
  3. L110
    trans ((((a) * (c))) + (((b) * (d))))
26Use earlier factsL111–111

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

  1. L111
    apply add_comm
27Calculate and transport equalitiesL112–120

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
    refl
  4. L115
    trans ((((a) * (a))) + ((((d) * (a))) + ((((b) * (b))) + ((((c) * (b))) + ((((d) * (d))) + ((((c) * (c))) + ((((a) * (b))) + ((((b) * (a))) + ((((c) * (d))) + ((((d) * (c))) + ((((a) * (c))) + (((b) * (d))))))))))))))
  5. L116
    symm
  6. L117
    congr
  7. L118
    refl
  8. L119
    congr
  9. L120
    trans ((a) * (d))
28Use earlier factsL121–121

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

  1. L121
    apply mul_comm
29Calculate and transport equalitiesL122–128

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

  1. L122
    congr
  2. L123
    refl
  3. L124
    refl
  4. L125
    congr
  5. L126
    refl
  6. L127
    congr
  7. L128
    trans ((b) * (c))
30Use earlier factsL129–129

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

  1. L129
    apply mul_comm
31Calculate and transport equalitiesL130–139

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

  1. L130
    congr
  2. L131
    refl
  3. L132
    refl
  4. L133
    congr
  5. L134
    refl
  6. L135
    congr
  7. L136
    refl
  8. L137
    congr
  9. L138
    refl
  10. L139
    congr
32Calculate and transport equalitiesL140–140

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

  1. L140
    trans ((a) * (b))
33Use earlier factsL141–141

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

  1. L141
    apply mul_comm
34Calculate and transport equalitiesL142–148

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
    congr
  5. L146
    refl
  6. L147
    congr
  7. L148
    trans ((c) * (d))
35Use earlier factsL149–149

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

  1. L149
    apply mul_comm
36Calculate and transport equalitiesL150–157

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

  1. L150
    congr
  2. L151
    refl
  3. L152
    refl
  4. L153
    congr
  5. L154
    refl
  6. L155
    refl
  7. L156
    symm
  8. L157
    simp [add_mul, mul_add, mul_assoc, add_assoc]
37Separate the logical casesL158–158

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

  1. L158
    split
38Calculate and transport equalitiesL159–159

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

  1. L159
    trans ((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
39Use earlier factsL160–160

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

  1. L160
    apply PA3
40Calculate and transport equalitiesL161–161

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

  1. L161
    trans ((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) + (N))
41Use earlier factsL162–163

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

  1. L162
    exact hreal
  2. L163
    apply add_comm
42Calculate and transport equalitiesL164–164

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

  1. L164
    trans ((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))
43Use earlier factsL165–165

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

  1. L165
    apply PA3
44Calculate and transport equalitiesL166–173

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

  1. L166
    trans ((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))
  2. L167
    trans ((((a) * (c))) + ((((d) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((d) * (a))) + ((((c) * (b))) + ((((d) * (d))) + (((c) * (c))))))))))
  3. L168
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  4. L169
    trans ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c))))))))))
  5. L170
    congr
  6. L171
    refl
  7. L172
    congr
  8. L173
    trans ((c) * (d))
45Use earlier factsL174–174

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

  1. L174
    apply mul_comm
46Calculate and transport equalitiesL175–183

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

  1. L175
    congr
  2. L176
    refl
  3. L177
    refl
  4. L178
    congr
  5. L179
    refl
  6. L180
    congr
  7. L181
    refl
  8. L182
    congr
  9. L183
    trans ((a) * (d))
47Use earlier factsL184–184

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

  1. L184
    apply mul_comm
48Calculate and transport equalitiesL185–189

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

  1. L185
    congr
  2. L186
    refl
  3. L187
    refl
  4. L188
    congr
  5. L189
    trans ((b) * (c))
49Use earlier factsL190–190

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

  1. L190
    apply mul_comm
50Calculate and transport equalitiesL191–200

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

  1. L191
    congr
  2. L192
    refl
  3. L193
    refl
  4. L194
    congr
  5. L195
    refl
  6. L196
    refl
  7. L197
    trans ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + ((((c) * (c))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))))))
  8. L198
    trans ((((a) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c))))))))))
  9. L199
    trans ((((a) * (c))) + ((((a) * (d))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c))))))))))
  10. L200
    congr
51Calculate and transport equalitiesL201–207

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

  1. L201
    refl
  2. L202
    trans ((((c) * (d))) + ((((a) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c)))))))))
  3. L203
    congr
  4. L204
    refl
  5. L205
    trans ((((b) * (d))) + ((((a) * (d))) + ((((c) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c))))))))
  6. L206
    congr
  7. L207
    refl
52Use earlier factsL208–211

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

  1. L208
    apply four_square_add_swap_right_tail
  2. L209
    apply four_square_add_swap_right_tail
  3. L210
    apply four_square_add_swap_right_tail
  4. L211
    apply four_square_add_swap_right_tail
53Calculate and transport equalitiesL212–221

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

  1. L212
    congr
  2. L213
    refl
  3. L214
    trans ((((d) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))
  4. L215
    trans ((((a) * (c))) + ((((d) * (d))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))
  5. L216
    congr
  6. L217
    refl
  7. L218
    trans ((((c) * (d))) + ((((d) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + (((c) * (c))))))))
  8. L219
    congr
  9. L220
    refl
  10. L221
    trans ((((b) * (d))) + ((((d) * (d))) + ((((c) * (d))) + ((((b) * (c))) + (((c) * (c)))))))
54Calculate and transport equalitiesL222–226

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

  1. L222
    congr
  2. L223
    refl
  3. L224
    trans ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))
  4. L225
    congr
  5. L226
    refl
55Use earlier factsL227–231

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

  1. L227
    apply four_square_add_swap_right_tail
  2. L228
    apply four_square_add_swap_right_tail
  3. L229
    apply four_square_add_swap_right_tail
  4. L230
    apply four_square_add_swap_right_tail
  5. L231
    apply four_square_add_swap_right_tail
56Calculate 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
    trans ((((b) * (c))) + ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + (((c) * (c))))))))
  4. L235
    trans ((((a) * (c))) + ((((b) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + (((c) * (c))))))))
  5. L236
    congr
  6. L237
    refl
  7. L238
    trans ((((c) * (d))) + ((((b) * (c))) + ((((b) * (d))) + ((((c) * (d))) + (((c) * (c)))))))
  8. L239
    congr
  9. L240
    refl
  10. L241
    trans ((((b) * (d))) + ((((b) * (c))) + ((((c) * (d))) + (((c) * (c))))))
57Calculate and transport equalitiesL242–243

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

  1. L242
    congr
  2. L243
    refl
58Use earlier factsL244–247

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

  1. L244
    apply four_square_add_swap_right_tail
  2. L245
    apply four_square_add_swap_right_tail
  3. L246
    apply four_square_add_swap_right_tail
  4. L247
    apply four_square_add_swap_right_tail
59Calculate and transport equalitiesL248–257

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

  1. L248
    congr
  2. L249
    refl
  3. L250
    trans ((((c) * (c))) + ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + (((c) * (d)))))))
  4. L251
    trans ((((a) * (c))) + ((((c) * (c))) + ((((c) * (d))) + ((((b) * (d))) + (((c) * (d)))))))
  5. L252
    congr
  6. L253
    refl
  7. L254
    trans ((((c) * (d))) + ((((c) * (c))) + ((((b) * (d))) + (((c) * (d))))))
  8. L255
    congr
  9. L256
    refl
  10. L257
    trans ((((b) * (d))) + ((((c) * (c))) + (((c) * (d)))))
60Calculate and transport equalitiesL258–259

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

  1. L258
    congr
  2. L259
    refl
61Use earlier factsL260–263

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

  1. L260
    apply add_comm
  2. L261
    apply four_square_add_swap_right_tail
  3. L262
    apply four_square_add_swap_right_tail
  4. L263
    apply four_square_add_swap_right_tail
62Calculate and transport equalitiesL264–269

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

  1. L264
    congr
  2. L265
    refl
  3. L266
    trans ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))
  4. L267
    trans ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + (((c) * (d))))))
  5. L268
    congr
  6. L269
    refl
63Use earlier factsL270–271

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

  1. L270
    apply four_square_add_swap_right_tail
  2. L271
    apply four_square_add_swap_right_tail
64Calculate and transport equalitiesL272–281

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

  1. L272
    congr
  2. L273
    refl
  3. L274
    refl
  4. L275
    trans ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + ((((c) * (c))) + ((((d) * (b))) + ((((c) * (a))) + ((((d) * (c))) + (((c) * (d))))))))))
  5. L276
    symm
  6. L277
    congr
  7. L278
    refl
  8. L279
    congr
  9. L280
    refl
  10. L281
    congr
65Calculate and transport equalitiesL282–286

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

  1. L282
    refl
  2. L283
    congr
  3. L284
    refl
  4. L285
    congr
  5. L286
    trans ((b) * (d))
66Use earlier factsL287–287

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

  1. L287
    apply mul_comm
67Calculate and transport equalitiesL288–292

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

  1. L288
    congr
  2. L289
    refl
  3. L290
    refl
  4. L291
    congr
  5. L292
    trans ((a) * (c))
68Use earlier factsL293–293

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

  1. L293
    apply mul_comm
69Calculate and transport equalitiesL294–298

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

  1. L294
    congr
  2. L295
    refl
  3. L296
    refl
  4. L297
    congr
  5. L298
    trans ((c) * (d))
70Use earlier factsL299–299

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

  1. L299
    apply mul_comm
71Calculate and transport equalitiesL300–306

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

  1. L300
    congr
  2. L301
    refl
  3. L302
    refl
  4. L303
    refl
  5. L304
    symm
  6. L305
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  7. L306
    symm
72Use earlier factsL307–307

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

  1. L307
    apply zero_add

Library-wide reading audit

Original defined command ledger · 307 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro N
  6. 0006intro hnorm
  7. 0007have hreal : ((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c)))))) = ((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) + (N))
  8. 0008specialize eisenstein_pair_natural_value_transport ((((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))) + (((((a) * (d))) + (((b) * (c))))))
  9. 0009specialize eisenstein_pair_natural_value_transport ((((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))) + (((((a) * (c))) + (((b) * (d))))))
  10. 0010specialize eisenstein_pair_natural_value_transport ((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
  11. 0011specialize eisenstein_pair_natural_value_transport ((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))
  12. 0012specialize eisenstein_pair_natural_value_transport N
  13. 0013apply eisenstein_pair_natural_value_transport
  14. 0014exact hnorm
  15. 0015trans ((((a) * (a))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((d) * (b))) + ((((b) * (a))) + ((((c) * (a))) + ((((d) * (c))) + (((c) * (d))))))))))))))
  16. 0016simp [add_mul, mul_add, mul_assoc, add_assoc]
  17. 0017trans ((((a) * (a))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))))))))))
  18. 0018congr
  19. 0019refl
  20. 0020congr
  21. 0021refl
  22. 0022congr
  23. 0023refl
  24. 0024congr
  25. 0025refl
  26. 0026congr
  27. 0027refl
  28. 0028congr
  29. 0029refl
  30. 0030congr
  31. 0031refl
  32. 0032congr
  33. 0033trans ((b) * (d))
  34. 0034apply mul_comm
  35. 0035congr
  36. 0036refl
  37. 0037refl
  38. 0038congr
  39. 0039trans ((a) * (b))
  40. 0040apply mul_comm
  41. 0041congr
  42. 0042refl
  43. 0043refl
  44. 0044congr
  45. 0045trans ((a) * (c))
  46. 0046apply mul_comm
  47. 0047congr
  48. 0048refl
  49. 0049refl
  50. 0050congr
  51. 0051trans ((c) * (d))
  52. 0052apply mul_comm
  53. 0053congr
  54. 0054refl
  55. 0055refl
  56. 0056refl
  57. 0057trans ((((a) * (a))) + ((((a) * (d))) + ((((b) * (b))) + ((((b) * (c))) + ((((d) * (d))) + ((((c) * (c))) + ((((a) * (b))) + ((((a) * (b))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (c))) + (((b) * (d))))))))))))))
  58. 0058congr
  59. 0059refl
  60. 0060trans ((((a) * (d))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))))))
  61. 0061trans ((((b) * (b))) + ((((a) * (d))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))))))
  62. 0062congr
  63. 0063refl
  64. 0064trans ((((c) * (c))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))))))))
  65. 0065congr
  66. 0066refl
  67. 0067apply four_square_add_swap_right_tail
  68. 0068apply four_square_add_swap_right_tail
  69. 0069apply four_square_add_swap_right_tail
  70. 0070congr
  71. 0071refl
  72. 0072congr
  73. 0073refl
  74. 0074trans ((((b) * (c))) + ((((c) * (c))) + ((((d) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))))
  75. 0075trans ((((c) * (c))) + ((((b) * (c))) + ((((d) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))))
  76. 0076congr
  77. 0077refl
  78. 0078apply four_square_add_swap_right_tail
  79. 0079apply four_square_add_swap_right_tail
  80. 0080congr
  81. 0081refl
  82. 0082trans ((((d) * (d))) + ((((c) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))))))
  83. 0083apply four_square_add_swap_right_tail
  84. 0084congr
  85. 0085refl
  86. 0086congr
  87. 0087refl
  88. 0088congr
  89. 0089refl
  90. 0090trans ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))
  91. 0091apply four_square_add_swap_right_tail
  92. 0092congr
  93. 0093refl
  94. 0094trans ((((c) * (d))) + ((((b) * (d))) + ((((a) * (c))) + (((c) * (d))))))
  95. 0095trans ((((b) * (d))) + ((((c) * (d))) + ((((a) * (c))) + (((c) * (d))))))
  96. 0096congr
  97. 0097refl
  98. 0098apply four_square_add_swap_right_tail
  99. 0099apply four_square_add_swap_right_tail
  100. 0100congr
  101. 0101refl
  102. 0102trans ((((c) * (d))) + ((((b) * (d))) + (((a) * (c)))))
  103. 0103trans ((((b) * (d))) + ((((c) * (d))) + (((a) * (c)))))
  104. 0104congr
  105. 0105refl
  106. 0106apply add_comm
  107. 0107apply four_square_add_swap_right_tail
  108. 0108congr
  109. 0109refl
  110. 0110trans ((((a) * (c))) + (((b) * (d))))
  111. 0111apply add_comm
  112. 0112congr
  113. 0113refl
  114. 0114refl
  115. 0115trans ((((a) * (a))) + ((((d) * (a))) + ((((b) * (b))) + ((((c) * (b))) + ((((d) * (d))) + ((((c) * (c))) + ((((a) * (b))) + ((((b) * (a))) + ((((c) * (d))) + ((((d) * (c))) + ((((a) * (c))) + (((b) * (d))))))))))))))
  116. 0116symm
  117. 0117congr
  118. 0118refl
  119. 0119congr
  120. 0120trans ((a) * (d))
  121. 0121apply mul_comm
  122. 0122congr
  123. 0123refl
  124. 0124refl
  125. 0125congr
  126. 0126refl
  127. 0127congr
  128. 0128trans ((b) * (c))
  129. 0129apply mul_comm
  130. 0130congr
  131. 0131refl
  132. 0132refl
  133. 0133congr
  134. 0134refl
  135. 0135congr
  136. 0136refl
  137. 0137congr
  138. 0138refl
  139. 0139congr
  140. 0140trans ((a) * (b))
  141. 0141apply mul_comm
  142. 0142congr
  143. 0143refl
  144. 0144refl
  145. 0145congr
  146. 0146refl
  147. 0147congr
  148. 0148trans ((c) * (d))
  149. 0149apply mul_comm
  150. 0150congr
  151. 0151refl
  152. 0152refl
  153. 0153congr
  154. 0154refl
  155. 0155refl
  156. 0156symm
  157. 0157simp [add_mul, mul_add, mul_assoc, add_assoc]
  158. 0158split
  159. 0159trans ((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
  160. 0160apply PA3
  161. 0161trans ((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) + (N))
  162. 0162exact hreal
  163. 0163apply add_comm
  164. 0164trans ((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))
  165. 0165apply PA3
  166. 0166trans ((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))
  167. 0167trans ((((a) * (c))) + ((((d) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((d) * (a))) + ((((c) * (b))) + ((((d) * (d))) + (((c) * (c))))))))))
  168. 0168simp [add_mul, mul_add, mul_assoc, add_assoc]
  169. 0169trans ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c))))))))))
  170. 0170congr
  171. 0171refl
  172. 0172congr
  173. 0173trans ((c) * (d))
  174. 0174apply mul_comm
  175. 0175congr
  176. 0176refl
  177. 0177refl
  178. 0178congr
  179. 0179refl
  180. 0180congr
  181. 0181refl
  182. 0182congr
  183. 0183trans ((a) * (d))
  184. 0184apply mul_comm
  185. 0185congr
  186. 0186refl
  187. 0187refl
  188. 0188congr
  189. 0189trans ((b) * (c))
  190. 0190apply mul_comm
  191. 0191congr
  192. 0192refl
  193. 0193refl
  194. 0194congr
  195. 0195refl
  196. 0196refl
  197. 0197trans ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + ((((c) * (c))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))))))
  198. 0198trans ((((a) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c))))))))))
  199. 0199trans ((((a) * (c))) + ((((a) * (d))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c))))))))))
  200. 0200congr
  201. 0201refl
  202. 0202trans ((((c) * (d))) + ((((a) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c)))))))))
  203. 0203congr
  204. 0204refl
  205. 0205trans ((((b) * (d))) + ((((a) * (d))) + ((((c) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c))))))))
  206. 0206congr
  207. 0207refl
  208. 0208apply four_square_add_swap_right_tail
  209. 0209apply four_square_add_swap_right_tail
  210. 0210apply four_square_add_swap_right_tail
  211. 0211apply four_square_add_swap_right_tail
  212. 0212congr
  213. 0213refl
  214. 0214trans ((((d) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))
  215. 0215trans ((((a) * (c))) + ((((d) * (d))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))
  216. 0216congr
  217. 0217refl
  218. 0218trans ((((c) * (d))) + ((((d) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((b) * (c))) + (((c) * (c))))))))
  219. 0219congr
  220. 0220refl
  221. 0221trans ((((b) * (d))) + ((((d) * (d))) + ((((c) * (d))) + ((((b) * (c))) + (((c) * (c)))))))
  222. 0222congr
  223. 0223refl
  224. 0224trans ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))
  225. 0225congr
  226. 0226refl
  227. 0227apply four_square_add_swap_right_tail
  228. 0228apply four_square_add_swap_right_tail
  229. 0229apply four_square_add_swap_right_tail
  230. 0230apply four_square_add_swap_right_tail
  231. 0231apply four_square_add_swap_right_tail
  232. 0232congr
  233. 0233refl
  234. 0234trans ((((b) * (c))) + ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + (((c) * (c))))))))
  235. 0235trans ((((a) * (c))) + ((((b) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + (((c) * (c))))))))
  236. 0236congr
  237. 0237refl
  238. 0238trans ((((c) * (d))) + ((((b) * (c))) + ((((b) * (d))) + ((((c) * (d))) + (((c) * (c)))))))
  239. 0239congr
  240. 0240refl
  241. 0241trans ((((b) * (d))) + ((((b) * (c))) + ((((c) * (d))) + (((c) * (c))))))
  242. 0242congr
  243. 0243refl
  244. 0244apply four_square_add_swap_right_tail
  245. 0245apply four_square_add_swap_right_tail
  246. 0246apply four_square_add_swap_right_tail
  247. 0247apply four_square_add_swap_right_tail
  248. 0248congr
  249. 0249refl
  250. 0250trans ((((c) * (c))) + ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + (((c) * (d)))))))
  251. 0251trans ((((a) * (c))) + ((((c) * (c))) + ((((c) * (d))) + ((((b) * (d))) + (((c) * (d)))))))
  252. 0252congr
  253. 0253refl
  254. 0254trans ((((c) * (d))) + ((((c) * (c))) + ((((b) * (d))) + (((c) * (d))))))
  255. 0255congr
  256. 0256refl
  257. 0257trans ((((b) * (d))) + ((((c) * (c))) + (((c) * (d)))))
  258. 0258congr
  259. 0259refl
  260. 0260apply add_comm
  261. 0261apply four_square_add_swap_right_tail
  262. 0262apply four_square_add_swap_right_tail
  263. 0263apply four_square_add_swap_right_tail
  264. 0264congr
  265. 0265refl
  266. 0266trans ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))
  267. 0267trans ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + (((c) * (d))))))
  268. 0268congr
  269. 0269refl
  270. 0270apply four_square_add_swap_right_tail
  271. 0271apply four_square_add_swap_right_tail
  272. 0272congr
  273. 0273refl
  274. 0274refl
  275. 0275trans ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + ((((c) * (c))) + ((((d) * (b))) + ((((c) * (a))) + ((((d) * (c))) + (((c) * (d))))))))))
  276. 0276symm
  277. 0277congr
  278. 0278refl
  279. 0279congr
  280. 0280refl
  281. 0281congr
  282. 0282refl
  283. 0283congr
  284. 0284refl
  285. 0285congr
  286. 0286trans ((b) * (d))
  287. 0287apply mul_comm
  288. 0288congr
  289. 0289refl
  290. 0290refl
  291. 0291congr
  292. 0292trans ((a) * (c))
  293. 0293apply mul_comm
  294. 0294congr
  295. 0295refl
  296. 0296refl
  297. 0297congr
  298. 0298trans ((c) * (d))
  299. 0299apply mul_comm
  300. 0300congr
  301. 0301refl
  302. 0302refl
  303. 0303refl
  304. 0304symm
  305. 0305simp [add_mul, mul_add, mul_assoc, add_assoc]
  306. 0306symm
  307. 0307apply zero_add