DF0007

dirichlet_grid_entry_transpose

Interchanging the first and last factors preserves an actual cell, by proved signed scalar interchange and a real factor-equation permutation.

Alpha v34 checked-use · first admitted v31 · 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.

Every grid, slice, row sum and intermediate table is constructed. Retained cells have witnessed n=(a*e)*c and value F(a)*(H(e)*G(c)). The flat endpoint is unused. Table associativity includes N=0 and compares only positive values, not encodings. Full G009 remains broader.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ H. ∀ n. ∀ a. ∀ e. ∀ z. DirichletGridEntry(F,G,H,n,a,e,z) → DirichletGridEntry(H,G,F,n,e,a,z)

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

Definition DAG

SignedMul(a,b,c) · 2DirichletGridEntry(F,G,H,n,a,e,z) · 2

Actual proof prerequisites

signed_mul_total · checked external prerequisitesigned_weighted_scalar_commute · checked external prerequisitedirichlet_grid_entry_from_factorizationmul_comm · checked external prerequisitedirichlet_grid_entry_omitted
Original expanded first-order statement 
forall F G H n a e z. ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_transpose_source dfg_first_transpose_source dfg_last_transpose_source dfg_value_transpose_source. (((n)=((a)*(e))*dfg_middle_transpose_source) /\ (((exists dst_positive_code_transpose_sourcefirst dst_positive_scale_transpose_sourcefirst dst_negative_code_transpose_sourcefirst dst_negative_scale_transpose_sourcefirst dst_positive_transpose_sourcefirst dst_negative_transpose_sourcefirst. (((F) = (((((dst_positive_code_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst)) * S ((dst_positive_code_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst)) + ((dst_positive_scale_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst))) + (((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) * S ((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) + ((dst_negative_scale_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)))) * S ((((dst_positive_code_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst)) * S ((dst_positive_code_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst)) + ((dst_positive_scale_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst))) + (((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) * S ((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) + ((dst_negative_scale_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)))) + ((((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) * S ((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) + ((dst_negative_scale_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst))) + (((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) * S ((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) + ((dst_negative_scale_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)))))) /\ (((((exists ff_h_pvs_transpose_sourcefirstpositive. ff_h_pvs_transpose_sourcefirstpositive + S (dst_positive_transpose_sourcefirst) = S ((S (a)) * dst_positive_scale_transpose_sourcefirst)) /\ exists ff_q_pvs_transpose_sourcefirstpositive. dst_positive_code_transpose_sourcefirst = ff_q_pvs_transpose_sourcefirstpositive * S ((S (a)) * dst_positive_scale_transpose_sourcefirst) + (dst_positive_transpose_sourcefirst))) /\ (((((exists ff_h_pvs_transpose_sourcefirstnegative. ff_h_pvs_transpose_sourcefirstnegative + S (dst_negative_transpose_sourcefirst) = S ((S (a)) * dst_negative_scale_transpose_sourcefirst)) /\ exists ff_q_pvs_transpose_sourcefirstnegative. dst_negative_code_transpose_sourcefirst = ff_q_pvs_transpose_sourcefirstnegative * S ((S (a)) * dst_negative_scale_transpose_sourcefirst) + (dst_negative_transpose_sourcefirst))) /\ (exists ge_balance_positive_transpose_sourcefirstvalue ge_balance_negative_transpose_sourcefirstvalue. (((((dfg_first_transpose_source) = 2 * (ge_balance_positive_transpose_sourcefirstvalue) /\ (ge_balance_negative_transpose_sourcefirstvalue) = 0) \/ exists ge_signed_half_transpose_sourcefirstvaluedecode. (((dfg_first_transpose_source) = 2 * ge_signed_half_transpose_sourcefirstvaluedecode + 1 /\ (ge_balance_positive_transpose_sourcefirstvalue) = 0) /\ (ge_balance_negative_transpose_sourcefirstvalue) = S ge_signed_half_transpose_sourcefirstvaluedecode))) /\ ((dst_positive_transpose_sourcefirst) + ge_balance_negative_transpose_sourcefirstvalue = (dst_negative_transpose_sourcefirst) + ge_balance_positive_transpose_sourcefirstvalue))))))))) /\ (((exists dst_positive_code_transpose_sourcelast dst_positive_scale_transpose_sourcelast dst_negative_code_transpose_sourcelast dst_negative_scale_transpose_sourcelast dst_positive_transpose_sourcelast dst_negative_transpose_sourcelast. (((H) = (((((dst_positive_code_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast)) * S ((dst_positive_code_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast)) + ((dst_positive_scale_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast))) + (((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) * S ((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) + ((dst_negative_scale_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)))) * S ((((dst_positive_code_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast)) * S ((dst_positive_code_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast)) + ((dst_positive_scale_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast))) + (((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) * S ((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) + ((dst_negative_scale_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)))) + ((((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) * S ((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) + ((dst_negative_scale_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast))) + (((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) * S ((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) + ((dst_negative_scale_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)))))) /\ (((((exists ff_h_pvs_transpose_sourcelastpositive. ff_h_pvs_transpose_sourcelastpositive + S (dst_positive_transpose_sourcelast) = S ((S (e)) * dst_positive_scale_transpose_sourcelast)) /\ exists ff_q_pvs_transpose_sourcelastpositive. dst_positive_code_transpose_sourcelast = ff_q_pvs_transpose_sourcelastpositive * S ((S (e)) * dst_positive_scale_transpose_sourcelast) + (dst_positive_transpose_sourcelast))) /\ (((((exists ff_h_pvs_transpose_sourcelastnegative. ff_h_pvs_transpose_sourcelastnegative + S (dst_negative_transpose_sourcelast) = S ((S (e)) * dst_negative_scale_transpose_sourcelast)) /\ exists ff_q_pvs_transpose_sourcelastnegative. dst_negative_code_transpose_sourcelast = ff_q_pvs_transpose_sourcelastnegative * S ((S (e)) * dst_negative_scale_transpose_sourcelast) + (dst_negative_transpose_sourcelast))) /\ (exists ge_balance_positive_transpose_sourcelastvalue ge_balance_negative_transpose_sourcelastvalue. (((((dfg_last_transpose_source) = 2 * (ge_balance_positive_transpose_sourcelastvalue) /\ (ge_balance_negative_transpose_sourcelastvalue) = 0) \/ exists ge_signed_half_transpose_sourcelastvaluedecode. (((dfg_last_transpose_source) = 2 * ge_signed_half_transpose_sourcelastvaluedecode + 1 /\ (ge_balance_positive_transpose_sourcelastvalue) = 0) /\ (ge_balance_negative_transpose_sourcelastvalue) = S ge_signed_half_transpose_sourcelastvaluedecode))) /\ ((dst_positive_transpose_sourcelast) + ge_balance_negative_transpose_sourcelastvalue = (dst_negative_transpose_sourcelast) + ge_balance_positive_transpose_sourcelastvalue))))))))) /\ (((exists dst_positive_code_transpose_sourcemiddle dst_positive_scale_transpose_sourcemiddle dst_negative_code_transpose_sourcemiddle dst_negative_scale_transpose_sourcemiddle dst_positive_transpose_sourcemiddle dst_negative_transpose_sourcemiddle. (((G) = (((((dst_positive_code_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle)) * S ((dst_positive_code_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle)) + ((dst_positive_scale_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle))) + (((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) * S ((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) + ((dst_negative_scale_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)))) * S ((((dst_positive_code_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle)) * S ((dst_positive_code_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle)) + ((dst_positive_scale_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle))) + (((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) * S ((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) + ((dst_negative_scale_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)))) + ((((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) * S ((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) + ((dst_negative_scale_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle))) + (((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) * S ((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) + ((dst_negative_scale_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)))))) /\ (((((exists ff_h_pvs_transpose_sourcemiddlepositive. ff_h_pvs_transpose_sourcemiddlepositive + S (dst_positive_transpose_sourcemiddle) = S ((S (dfg_middle_transpose_source)) * dst_positive_scale_transpose_sourcemiddle)) /\ exists ff_q_pvs_transpose_sourcemiddlepositive. dst_positive_code_transpose_sourcemiddle = ff_q_pvs_transpose_sourcemiddlepositive * S ((S (dfg_middle_transpose_source)) * dst_positive_scale_transpose_sourcemiddle) + (dst_positive_transpose_sourcemiddle))) /\ (((((exists ff_h_pvs_transpose_sourcemiddlenegative. ff_h_pvs_transpose_sourcemiddlenegative + S (dst_negative_transpose_sourcemiddle) = S ((S (dfg_middle_transpose_source)) * dst_negative_scale_transpose_sourcemiddle)) /\ exists ff_q_pvs_transpose_sourcemiddlenegative. dst_negative_code_transpose_sourcemiddle = ff_q_pvs_transpose_sourcemiddlenegative * S ((S (dfg_middle_transpose_source)) * dst_negative_scale_transpose_sourcemiddle) + (dst_negative_transpose_sourcemiddle))) /\ (exists ge_balance_positive_transpose_sourcemiddlevalue ge_balance_negative_transpose_sourcemiddlevalue. (((((dfg_value_transpose_source) = 2 * (ge_balance_positive_transpose_sourcemiddlevalue) /\ (ge_balance_negative_transpose_sourcemiddlevalue) = 0) \/ exists ge_signed_half_transpose_sourcemiddlevaluedecode. (((dfg_value_transpose_source) = 2 * ge_signed_half_transpose_sourcemiddlevaluedecode + 1 /\ (ge_balance_positive_transpose_sourcemiddlevalue) = 0) /\ (ge_balance_negative_transpose_sourcemiddlevalue) = S ge_signed_half_transpose_sourcemiddlevaluedecode))) /\ ((dst_positive_transpose_sourcemiddle) + ge_balance_negative_transpose_sourcemiddlevalue = (dst_negative_transpose_sourcemiddle) + ge_balance_positive_transpose_sourcemiddlevalue))))))))) /\ (exists dfg_inner_transpose_sourceproduct. ((exists sto_ap_transpose_sourceproductinner sto_an_transpose_sourceproductinner sto_bp_transpose_sourceproductinner sto_bn_transpose_sourceproductinner sto_cp_transpose_sourceproductinner sto_cn_transpose_sourceproductinner. (((((dfg_last_transpose_source) = 2 * (sto_ap_transpose_sourceproductinner) /\ (sto_an_transpose_sourceproductinner) = 0) \/ exists ge_signed_half_transpose_sourceproductinnerleft. (((dfg_last_transpose_source) = 2 * ge_signed_half_transpose_sourceproductinnerleft + 1 /\ (sto_ap_transpose_sourceproductinner) = 0) /\ (sto_an_transpose_sourceproductinner) = S ge_signed_half_transpose_sourceproductinnerleft))) /\ ((((((dfg_value_transpose_source) = 2 * (sto_bp_transpose_sourceproductinner) /\ (sto_bn_transpose_sourceproductinner) = 0) \/ exists ge_signed_half_transpose_sourceproductinnerright. (((dfg_value_transpose_source) = 2 * ge_signed_half_transpose_sourceproductinnerright + 1 /\ (sto_bp_transpose_sourceproductinner) = 0) /\ (sto_bn_transpose_sourceproductinner) = S ge_signed_half_transpose_sourceproductinnerright))) /\ ((((((dfg_inner_transpose_sourceproduct) = 2 * (sto_cp_transpose_sourceproductinner) /\ (sto_cn_transpose_sourceproductinner) = 0) \/ exists ge_signed_half_transpose_sourceproductinneroutput. (((dfg_inner_transpose_sourceproduct) = 2 * ge_signed_half_transpose_sourceproductinneroutput + 1 /\ (sto_cp_transpose_sourceproductinner) = 0) /\ (sto_cn_transpose_sourceproductinner) = S ge_signed_half_transpose_sourceproductinneroutput))) /\ ((sto_ap_transpose_sourceproductinner * sto_bp_transpose_sourceproductinner + sto_an_transpose_sourceproductinner * sto_bn_transpose_sourceproductinner) + sto_cn_transpose_sourceproductinner = (sto_ap_transpose_sourceproductinner * sto_bn_transpose_sourceproductinner + sto_an_transpose_sourceproductinner * sto_bp_transpose_sourceproductinner) + sto_cp_transpose_sourceproductinner))))))) /\ (exists sto_ap_transpose_sourceproductouter sto_an_transpose_sourceproductouter sto_bp_transpose_sourceproductouter sto_bn_transpose_sourceproductouter sto_cp_transpose_sourceproductouter sto_cn_transpose_sourceproductouter. (((((dfg_first_transpose_source) = 2 * (sto_ap_transpose_sourceproductouter) /\ (sto_an_transpose_sourceproductouter) = 0) \/ exists ge_signed_half_transpose_sourceproductouterleft. (((dfg_first_transpose_source) = 2 * ge_signed_half_transpose_sourceproductouterleft + 1 /\ (sto_ap_transpose_sourceproductouter) = 0) /\ (sto_an_transpose_sourceproductouter) = S ge_signed_half_transpose_sourceproductouterleft))) /\ ((((((dfg_inner_transpose_sourceproduct) = 2 * (sto_bp_transpose_sourceproductouter) /\ (sto_bn_transpose_sourceproductouter) = 0) \/ exists ge_signed_half_transpose_sourceproductouterright. (((dfg_inner_transpose_sourceproduct) = 2 * ge_signed_half_transpose_sourceproductouterright + 1 /\ (sto_bp_transpose_sourceproductouter) = 0) /\ (sto_bn_transpose_sourceproductouter) = S ge_signed_half_transpose_sourceproductouterright))) /\ ((((((z) = 2 * (sto_cp_transpose_sourceproductouter) /\ (sto_cn_transpose_sourceproductouter) = 0) \/ exists ge_signed_half_transpose_sourceproductouteroutput. (((z) = 2 * ge_signed_half_transpose_sourceproductouteroutput + 1 /\ (sto_cp_transpose_sourceproductouter) = 0) /\ (sto_cn_transpose_sourceproductouter) = S ge_signed_half_transpose_sourceproductouteroutput))) /\ ((sto_ap_transpose_sourceproductouter * sto_bp_transpose_sourceproductouter + sto_an_transpose_sourceproductouter * sto_bn_transpose_sourceproductouter) + sto_cn_transpose_sourceproductouter = (sto_ap_transpose_sourceproductouter * sto_bn_transpose_sourceproductouter + sto_an_transpose_sourceproductouter * sto_bp_transpose_sourceproductouter) + sto_cp_transpose_sourceproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_transpose_sourceomittednondivisor. (n) = ((a)*(e)) * pvs_factor_transpose_sourceomittednondivisor))) /\ ((z)=0)))) -> ((((~((e)=0)) /\ (((~((a)=0)) /\ (exists dfg_middle_transpose_target dfg_first_transpose_target dfg_last_transpose_target dfg_value_transpose_target. (((n)=((e)*(a))*dfg_middle_transpose_target) /\ (((exists dst_positive_code_transpose_targetfirst dst_positive_scale_transpose_targetfirst dst_negative_code_transpose_targetfirst dst_negative_scale_transpose_targetfirst dst_positive_transpose_targetfirst dst_negative_transpose_targetfirst. (((H) = (((((dst_positive_code_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst)) * S ((dst_positive_code_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst)) + ((dst_positive_scale_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst))) + (((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) * S ((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) + ((dst_negative_scale_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)))) * S ((((dst_positive_code_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst)) * S ((dst_positive_code_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst)) + ((dst_positive_scale_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst))) + (((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) * S ((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) + ((dst_negative_scale_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)))) + ((((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) * S ((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) + ((dst_negative_scale_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst))) + (((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) * S ((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) + ((dst_negative_scale_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)))))) /\ (((((exists ff_h_pvs_transpose_targetfirstpositive. ff_h_pvs_transpose_targetfirstpositive + S (dst_positive_transpose_targetfirst) = S ((S (e)) * dst_positive_scale_transpose_targetfirst)) /\ exists ff_q_pvs_transpose_targetfirstpositive. dst_positive_code_transpose_targetfirst = ff_q_pvs_transpose_targetfirstpositive * S ((S (e)) * dst_positive_scale_transpose_targetfirst) + (dst_positive_transpose_targetfirst))) /\ (((((exists ff_h_pvs_transpose_targetfirstnegative. ff_h_pvs_transpose_targetfirstnegative + S (dst_negative_transpose_targetfirst) = S ((S (e)) * dst_negative_scale_transpose_targetfirst)) /\ exists ff_q_pvs_transpose_targetfirstnegative. dst_negative_code_transpose_targetfirst = ff_q_pvs_transpose_targetfirstnegative * S ((S (e)) * dst_negative_scale_transpose_targetfirst) + (dst_negative_transpose_targetfirst))) /\ (exists ge_balance_positive_transpose_targetfirstvalue ge_balance_negative_transpose_targetfirstvalue. (((((dfg_first_transpose_target) = 2 * (ge_balance_positive_transpose_targetfirstvalue) /\ (ge_balance_negative_transpose_targetfirstvalue) = 0) \/ exists ge_signed_half_transpose_targetfirstvaluedecode. (((dfg_first_transpose_target) = 2 * ge_signed_half_transpose_targetfirstvaluedecode + 1 /\ (ge_balance_positive_transpose_targetfirstvalue) = 0) /\ (ge_balance_negative_transpose_targetfirstvalue) = S ge_signed_half_transpose_targetfirstvaluedecode))) /\ ((dst_positive_transpose_targetfirst) + ge_balance_negative_transpose_targetfirstvalue = (dst_negative_transpose_targetfirst) + ge_balance_positive_transpose_targetfirstvalue))))))))) /\ (((exists dst_positive_code_transpose_targetlast dst_positive_scale_transpose_targetlast dst_negative_code_transpose_targetlast dst_negative_scale_transpose_targetlast dst_positive_transpose_targetlast dst_negative_transpose_targetlast. (((F) = (((((dst_positive_code_transpose_targetlast) + (dst_positive_scale_transpose_targetlast)) * S ((dst_positive_code_transpose_targetlast) + (dst_positive_scale_transpose_targetlast)) + ((dst_positive_scale_transpose_targetlast) + (dst_positive_scale_transpose_targetlast))) + (((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) * S ((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) + ((dst_negative_scale_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)))) * S ((((dst_positive_code_transpose_targetlast) + (dst_positive_scale_transpose_targetlast)) * S ((dst_positive_code_transpose_targetlast) + (dst_positive_scale_transpose_targetlast)) + ((dst_positive_scale_transpose_targetlast) + (dst_positive_scale_transpose_targetlast))) + (((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) * S ((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) + ((dst_negative_scale_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)))) + ((((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) * S ((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) + ((dst_negative_scale_transpose_targetlast) + (dst_negative_scale_transpose_targetlast))) + (((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) * S ((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) + ((dst_negative_scale_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)))))) /\ (((((exists ff_h_pvs_transpose_targetlastpositive. ff_h_pvs_transpose_targetlastpositive + S (dst_positive_transpose_targetlast) = S ((S (a)) * dst_positive_scale_transpose_targetlast)) /\ exists ff_q_pvs_transpose_targetlastpositive. dst_positive_code_transpose_targetlast = ff_q_pvs_transpose_targetlastpositive * S ((S (a)) * dst_positive_scale_transpose_targetlast) + (dst_positive_transpose_targetlast))) /\ (((((exists ff_h_pvs_transpose_targetlastnegative. ff_h_pvs_transpose_targetlastnegative + S (dst_negative_transpose_targetlast) = S ((S (a)) * dst_negative_scale_transpose_targetlast)) /\ exists ff_q_pvs_transpose_targetlastnegative. dst_negative_code_transpose_targetlast = ff_q_pvs_transpose_targetlastnegative * S ((S (a)) * dst_negative_scale_transpose_targetlast) + (dst_negative_transpose_targetlast))) /\ (exists ge_balance_positive_transpose_targetlastvalue ge_balance_negative_transpose_targetlastvalue. (((((dfg_last_transpose_target) = 2 * (ge_balance_positive_transpose_targetlastvalue) /\ (ge_balance_negative_transpose_targetlastvalue) = 0) \/ exists ge_signed_half_transpose_targetlastvaluedecode. (((dfg_last_transpose_target) = 2 * ge_signed_half_transpose_targetlastvaluedecode + 1 /\ (ge_balance_positive_transpose_targetlastvalue) = 0) /\ (ge_balance_negative_transpose_targetlastvalue) = S ge_signed_half_transpose_targetlastvaluedecode))) /\ ((dst_positive_transpose_targetlast) + ge_balance_negative_transpose_targetlastvalue = (dst_negative_transpose_targetlast) + ge_balance_positive_transpose_targetlastvalue))))))))) /\ (((exists dst_positive_code_transpose_targetmiddle dst_positive_scale_transpose_targetmiddle dst_negative_code_transpose_targetmiddle dst_negative_scale_transpose_targetmiddle dst_positive_transpose_targetmiddle dst_negative_transpose_targetmiddle. (((G) = (((((dst_positive_code_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle)) * S ((dst_positive_code_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle)) + ((dst_positive_scale_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle))) + (((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) * S ((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) + ((dst_negative_scale_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)))) * S ((((dst_positive_code_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle)) * S ((dst_positive_code_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle)) + ((dst_positive_scale_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle))) + (((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) * S ((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) + ((dst_negative_scale_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)))) + ((((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) * S ((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) + ((dst_negative_scale_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle))) + (((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) * S ((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) + ((dst_negative_scale_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)))))) /\ (((((exists ff_h_pvs_transpose_targetmiddlepositive. ff_h_pvs_transpose_targetmiddlepositive + S (dst_positive_transpose_targetmiddle) = S ((S (dfg_middle_transpose_target)) * dst_positive_scale_transpose_targetmiddle)) /\ exists ff_q_pvs_transpose_targetmiddlepositive. dst_positive_code_transpose_targetmiddle = ff_q_pvs_transpose_targetmiddlepositive * S ((S (dfg_middle_transpose_target)) * dst_positive_scale_transpose_targetmiddle) + (dst_positive_transpose_targetmiddle))) /\ (((((exists ff_h_pvs_transpose_targetmiddlenegative. ff_h_pvs_transpose_targetmiddlenegative + S (dst_negative_transpose_targetmiddle) = S ((S (dfg_middle_transpose_target)) * dst_negative_scale_transpose_targetmiddle)) /\ exists ff_q_pvs_transpose_targetmiddlenegative. dst_negative_code_transpose_targetmiddle = ff_q_pvs_transpose_targetmiddlenegative * S ((S (dfg_middle_transpose_target)) * dst_negative_scale_transpose_targetmiddle) + (dst_negative_transpose_targetmiddle))) /\ (exists ge_balance_positive_transpose_targetmiddlevalue ge_balance_negative_transpose_targetmiddlevalue. (((((dfg_value_transpose_target) = 2 * (ge_balance_positive_transpose_targetmiddlevalue) /\ (ge_balance_negative_transpose_targetmiddlevalue) = 0) \/ exists ge_signed_half_transpose_targetmiddlevaluedecode. (((dfg_value_transpose_target) = 2 * ge_signed_half_transpose_targetmiddlevaluedecode + 1 /\ (ge_balance_positive_transpose_targetmiddlevalue) = 0) /\ (ge_balance_negative_transpose_targetmiddlevalue) = S ge_signed_half_transpose_targetmiddlevaluedecode))) /\ ((dst_positive_transpose_targetmiddle) + ge_balance_negative_transpose_targetmiddlevalue = (dst_negative_transpose_targetmiddle) + ge_balance_positive_transpose_targetmiddlevalue))))))))) /\ (exists dfg_inner_transpose_targetproduct. ((exists sto_ap_transpose_targetproductinner sto_an_transpose_targetproductinner sto_bp_transpose_targetproductinner sto_bn_transpose_targetproductinner sto_cp_transpose_targetproductinner sto_cn_transpose_targetproductinner. (((((dfg_last_transpose_target) = 2 * (sto_ap_transpose_targetproductinner) /\ (sto_an_transpose_targetproductinner) = 0) \/ exists ge_signed_half_transpose_targetproductinnerleft. (((dfg_last_transpose_target) = 2 * ge_signed_half_transpose_targetproductinnerleft + 1 /\ (sto_ap_transpose_targetproductinner) = 0) /\ (sto_an_transpose_targetproductinner) = S ge_signed_half_transpose_targetproductinnerleft))) /\ ((((((dfg_value_transpose_target) = 2 * (sto_bp_transpose_targetproductinner) /\ (sto_bn_transpose_targetproductinner) = 0) \/ exists ge_signed_half_transpose_targetproductinnerright. (((dfg_value_transpose_target) = 2 * ge_signed_half_transpose_targetproductinnerright + 1 /\ (sto_bp_transpose_targetproductinner) = 0) /\ (sto_bn_transpose_targetproductinner) = S ge_signed_half_transpose_targetproductinnerright))) /\ ((((((dfg_inner_transpose_targetproduct) = 2 * (sto_cp_transpose_targetproductinner) /\ (sto_cn_transpose_targetproductinner) = 0) \/ exists ge_signed_half_transpose_targetproductinneroutput. (((dfg_inner_transpose_targetproduct) = 2 * ge_signed_half_transpose_targetproductinneroutput + 1 /\ (sto_cp_transpose_targetproductinner) = 0) /\ (sto_cn_transpose_targetproductinner) = S ge_signed_half_transpose_targetproductinneroutput))) /\ ((sto_ap_transpose_targetproductinner * sto_bp_transpose_targetproductinner + sto_an_transpose_targetproductinner * sto_bn_transpose_targetproductinner) + sto_cn_transpose_targetproductinner = (sto_ap_transpose_targetproductinner * sto_bn_transpose_targetproductinner + sto_an_transpose_targetproductinner * sto_bp_transpose_targetproductinner) + sto_cp_transpose_targetproductinner))))))) /\ (exists sto_ap_transpose_targetproductouter sto_an_transpose_targetproductouter sto_bp_transpose_targetproductouter sto_bn_transpose_targetproductouter sto_cp_transpose_targetproductouter sto_cn_transpose_targetproductouter. (((((dfg_first_transpose_target) = 2 * (sto_ap_transpose_targetproductouter) /\ (sto_an_transpose_targetproductouter) = 0) \/ exists ge_signed_half_transpose_targetproductouterleft. (((dfg_first_transpose_target) = 2 * ge_signed_half_transpose_targetproductouterleft + 1 /\ (sto_ap_transpose_targetproductouter) = 0) /\ (sto_an_transpose_targetproductouter) = S ge_signed_half_transpose_targetproductouterleft))) /\ ((((((dfg_inner_transpose_targetproduct) = 2 * (sto_bp_transpose_targetproductouter) /\ (sto_bn_transpose_targetproductouter) = 0) \/ exists ge_signed_half_transpose_targetproductouterright. (((dfg_inner_transpose_targetproduct) = 2 * ge_signed_half_transpose_targetproductouterright + 1 /\ (sto_bp_transpose_targetproductouter) = 0) /\ (sto_bn_transpose_targetproductouter) = S ge_signed_half_transpose_targetproductouterright))) /\ ((((((z) = 2 * (sto_cp_transpose_targetproductouter) /\ (sto_cn_transpose_targetproductouter) = 0) \/ exists ge_signed_half_transpose_targetproductouteroutput. (((z) = 2 * ge_signed_half_transpose_targetproductouteroutput + 1 /\ (sto_cp_transpose_targetproductouter) = 0) /\ (sto_cn_transpose_targetproductouter) = S ge_signed_half_transpose_targetproductouteroutput))) /\ ((sto_ap_transpose_targetproductouter * sto_bp_transpose_targetproductouter + sto_an_transpose_targetproductouter * sto_bn_transpose_targetproductouter) + sto_cn_transpose_targetproductouter = (sto_ap_transpose_targetproductouter * sto_bn_transpose_targetproductouter + sto_an_transpose_targetproductouter * sto_bp_transpose_targetproductouter) + sto_cp_transpose_targetproductouter))))))))))))))))))))) \/ ((((e)=0 \/ ((a)=0 \/ ~(exists pvs_factor_transpose_targetomittednondivisor. (n) = ((e)*(a)) * pvs_factor_transpose_targetomittednondivisor))) /\ ((z)=0))))

Complete tactic proof in conservative notation

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

91 script commands · 31 reading checkpoints · 2 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)
dirichlet grid entry from factorizationdirichlet grid entry omitted
01Fix variables and assumptionsL1–8

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro H
  4. L4
    intro n
  5. L5
    intro a
  6. L6
    intro e
  7. L7
    intro z
  8. L8
    intro hv
02Separate the logical casesL9–18

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

  1. L9
    cases hv
  2. L10
    cases hv_left
  3. L11
    cases hv_left_right
  4. L12
    cases hv_left_right_right
  5. L13
    cases hv_left_right_right_witness
  6. L14
    cases hv_left_right_right_witness_witness
  7. L15
    cases hv_left_right_right_witness_witness_witness
  8. L16
    cases hv_left_right_right_witness_witness_witness_witness
  9. L17
    cases hv_left_right_right_witness_witness_witness_witness_right
  10. L18
    cases hv_left_right_right_witness_witness_witness_witness_right_right
03Separate the logical casesL19–21

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

  1. L19
    cases hv_left_right_right_witness_witness_witness_witness_right_right_right
  2. L20
    cases hv_left_right_right_witness_witness_witness_witness_right_right_right_right
  3. L21
    cases hv_left_right_right_witness_witness_witness_witness_right_right_right_right_witness
04Establish hiL22–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed mul total.

  1. L22
    have hi : ∃ r. SignedMul(x1,x3,r)Definitions: SignedMul(x1,x3,r)Original native command in the exact edition
  2. L23
    specialize signed_mul_total (x1)
  3. L24
    specialize signed_mul_total (x3)
  4. L25
    apply signed_mul_total
05Separate the logical casesL26–26

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

  1. L26
    cases hi
06Establish hoL27–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed weighted scalar commute.

  1. L27
  2. L28
    specialize signed_weighted_scalar_commute (x2)
  3. L29
    specialize signed_weighted_scalar_commute (x3)
  4. L30
    specialize signed_weighted_scalar_commute (x1)
  5. L31
    specialize signed_weighted_scalar_commute (x4)
  6. L32
    specialize signed_weighted_scalar_commute (x5)
  7. L33
    specialize signed_weighted_scalar_commute (z)
  8. L34
    apply signed_weighted_scalar_commute
  9. L35
    exact hv_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_left
  10. L36
    exact hi_witness
07Use earlier factsL37–46

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

  1. L37
    exact hv_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_right
  2. L38
    specialize dirichlet_grid_entry_from_factorization (H)
  3. L39
    specialize dirichlet_grid_entry_from_factorization (G)
  4. L40
    specialize dirichlet_grid_entry_from_factorization (F)
  5. L41
    specialize dirichlet_grid_entry_from_factorization (n)
  6. L42
    specialize dirichlet_grid_entry_from_factorization (e)
  7. L43
    specialize dirichlet_grid_entry_from_factorization (a)
  8. L44
    specialize dirichlet_grid_entry_from_factorization (x)
  9. L45
    specialize dirichlet_grid_entry_from_factorization (x2)
  10. L46
    specialize dirichlet_grid_entry_from_factorization (x1)
08Use earlier factsL47–52

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

  1. L47
    specialize dirichlet_grid_entry_from_factorization (x3)
  2. L48
    specialize dirichlet_grid_entry_from_factorization (x5)
  3. L49
    specialize dirichlet_grid_entry_from_factorization (z)
  4. L50
    apply dirichlet_grid_entry_from_factorization
  5. L51
    exact hv_left_right_left
  6. L52
    exact hv_left_left
09Calculate and transport equalitiesL53–53

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

  1. L53
    trans (a*e)*x
10Use earlier factsL54–54

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

  1. L54
    exact hv_left_right_right_witness_witness_witness_witness_left
11Calculate and transport equalitiesL55–55

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

  1. L55
    congr
12Use earlier factsL56–56

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

  1. L56
    apply mul_comm
13Calculate and transport equalitiesL57–57

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

  1. L57
    refl
14Use earlier factsL58–62

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

  1. L58
    exact hv_left_right_right_witness_witness_witness_witness_right_right_left
  2. L59
    exact hv_left_right_right_witness_witness_witness_witness_right_left
  3. L60
    exact hv_left_right_right_witness_witness_witness_witness_right_right_right_left
  4. L61
    exact hi_witness
  5. L62
    exact ho
15Separate the logical casesL63–63

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

  1. L63
    cases hv_right
16Calculate and transport equalitiesL64–66

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

  1. L64
    rewrite hv_right_right
  2. L65
    rewrite hv_right_right
  3. L66
    rewrite hv_right_right
17Use earlier factsL67–73

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

  1. L67
    specialize dirichlet_grid_entry_omitted (H)
  2. L68
    specialize dirichlet_grid_entry_omitted (G)
  3. L69
    specialize dirichlet_grid_entry_omitted (F)
  4. L70
    specialize dirichlet_grid_entry_omitted (n)
  5. L71
    specialize dirichlet_grid_entry_omitted (e)
  6. L72
    specialize dirichlet_grid_entry_omitted (a)
  7. L73
    apply dirichlet_grid_entry_omitted
18Separate the logical casesL74–76

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

  1. L74
    cases hv_right_left
  2. L75
    right
  3. L76
    left
19Use earlier factsL77–77

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

  1. L77
    exact hv_right_left_left
20Separate the logical casesL78–79

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

  1. L78
    cases hv_right_left_right
  2. L79
    left
21Use earlier factsL80–80

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

  1. L80
    exact hv_right_left_right_left
22Separate the logical casesL81–82

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

  1. L81
    right
  2. L82
    right
23Fix variables and assumptionsL83–83

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

  1. L83
    intro hd
24Separate the logical casesL84–84

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

  1. L84
    cases hd
25Use earlier factsL85–85

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

  1. L85
    apply hv_right_left_right_right
26Construct an explicit witnessL86–86

Supply the displayed value, then prove that it has the required property.

  1. L86
    exists x
27Calculate and transport equalitiesL87–87

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

  1. L87
    trans (e*a)*x
28Use earlier factsL88–88

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

  1. L88
    exact hd_witness
29Calculate and transport equalitiesL89–89

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

  1. L89
    congr
30Use earlier factsL90–90

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

  1. L90
    apply mul_comm
31Calculate and transport equalitiesL91–91

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

  1. L91
    refl

Library-wide reading audit

Original defined command ledger · 91 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro n
  5. 0005intro a
  6. 0006intro e
  7. 0007intro z
  8. 0008intro hv
  9. 0009cases hv
  10. 0010cases hv_left
  11. 0011cases hv_left_right
  12. 0012cases hv_left_right_right
  13. 0013cases hv_left_right_right_witness
  14. 0014cases hv_left_right_right_witness_witness
  15. 0015cases hv_left_right_right_witness_witness_witness
  16. 0016cases hv_left_right_right_witness_witness_witness_witness
  17. 0017cases hv_left_right_right_witness_witness_witness_witness_right
  18. 0018cases hv_left_right_right_witness_witness_witness_witness_right_right
  19. 0019cases hv_left_right_right_witness_witness_witness_witness_right_right_right
  20. 0020cases hv_left_right_right_witness_witness_witness_witness_right_right_right_right
  21. 0021cases hv_left_right_right_witness_witness_witness_witness_right_right_right_right_witness
  22. 0022have hi : ∃ r. SignedMul(x1,x3,r)
  23. 0023specialize signed_mul_total (x1)
  24. 0024specialize signed_mul_total (x3)
  25. 0025apply signed_mul_total
  26. 0026cases hi
  27. 0027have ho : SignedMul(x2,x5,z)
  28. 0028specialize signed_weighted_scalar_commute (x2)
  29. 0029specialize signed_weighted_scalar_commute (x3)
  30. 0030specialize signed_weighted_scalar_commute (x1)
  31. 0031specialize signed_weighted_scalar_commute (x4)
  32. 0032specialize signed_weighted_scalar_commute (x5)
  33. 0033specialize signed_weighted_scalar_commute (z)
  34. 0034apply signed_weighted_scalar_commute
  35. 0035exact hv_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_left
  36. 0036exact hi_witness
  37. 0037exact hv_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_right
  38. 0038specialize dirichlet_grid_entry_from_factorization (H)
  39. 0039specialize dirichlet_grid_entry_from_factorization (G)
  40. 0040specialize dirichlet_grid_entry_from_factorization (F)
  41. 0041specialize dirichlet_grid_entry_from_factorization (n)
  42. 0042specialize dirichlet_grid_entry_from_factorization (e)
  43. 0043specialize dirichlet_grid_entry_from_factorization (a)
  44. 0044specialize dirichlet_grid_entry_from_factorization (x)
  45. 0045specialize dirichlet_grid_entry_from_factorization (x2)
  46. 0046specialize dirichlet_grid_entry_from_factorization (x1)
  47. 0047specialize dirichlet_grid_entry_from_factorization (x3)
  48. 0048specialize dirichlet_grid_entry_from_factorization (x5)
  49. 0049specialize dirichlet_grid_entry_from_factorization (z)
  50. 0050apply dirichlet_grid_entry_from_factorization
  51. 0051exact hv_left_right_left
  52. 0052exact hv_left_left
  53. 0053trans (a*e)*x
  54. 0054exact hv_left_right_right_witness_witness_witness_witness_left
  55. 0055congr
  56. 0056apply mul_comm
  57. 0057refl
  58. 0058exact hv_left_right_right_witness_witness_witness_witness_right_right_left
  59. 0059exact hv_left_right_right_witness_witness_witness_witness_right_left
  60. 0060exact hv_left_right_right_witness_witness_witness_witness_right_right_right_left
  61. 0061exact hi_witness
  62. 0062exact ho
  63. 0063cases hv_right
  64. 0064rewrite hv_right_right
  65. 0065rewrite hv_right_right
  66. 0066rewrite hv_right_right
  67. 0067specialize dirichlet_grid_entry_omitted (H)
  68. 0068specialize dirichlet_grid_entry_omitted (G)
  69. 0069specialize dirichlet_grid_entry_omitted (F)
  70. 0070specialize dirichlet_grid_entry_omitted (n)
  71. 0071specialize dirichlet_grid_entry_omitted (e)
  72. 0072specialize dirichlet_grid_entry_omitted (a)
  73. 0073apply dirichlet_grid_entry_omitted
  74. 0074cases hv_right_left
  75. 0075right
  76. 0076left
  77. 0077exact hv_right_left_left
  78. 0078cases hv_right_left_right
  79. 0079left
  80. 0080exact hv_right_left_right_left
  81. 0081right
  82. 0082right
  83. 0083intro hd
  84. 0084cases hd
  85. 0085apply hv_right_left_right_right
  86. 0086exists x
  87. 0087trans (e*a)*x
  88. 0088exact hd_witness
  89. 0089congr
  90. 0090apply mul_comm
  91. 0091refl