mul_right_cancel
plain-language theorem explainer
Right multiplication cancellation holds on the Grothendieck completion LogicInt: if c is nonzero and a*c equals b*c then a equals b. Researchers constructing the integers and rationals from the Law of Logic cite this when verifying that LogicInt behaves as an integral domain. The tactic proof transfers the statement to the standard integers via eq_iff_toInt_eq and toInt_mul, applies Int.eq_of_mul_eq_mul_right, and transfers the conclusion back.
Claim. Let $a, b, c$ belong to the Grothendieck completion LogicInt of LogicNat. If $c$ is nonzero and $a c = b c$, then $a = b$.
background
LogicInt is the quotient of LogicNat pairs under the Grothendieck equivalence for addition, constructed without presupposing the integers. The transfer principle eq_iff_toInt_eq states that an equality holds in LogicInt precisely when the images under toInt are equal in the standard integers. LogicNat itself is the inductive type generated by an identity element and a successor step, mirroring the orbit closed under multiplication by the generator from the Law of Logic.
proof idea
The tactic first derives toInt c ≠ 0 from c ≠ 0 by rewriting with eq_iff_toInt_eq and toInt_zero. It then rewrites the hypothesis ac = bc using eq_iff_toInt_eq and toInt_mul to obtain an equality in Int, applies Int.eq_of_mul_eq_mul_right, and finally rewrites the resulting equality back via eq_iff_toInt_eq.
why it matters
This lemma supplies the cancellation needed to build the ring structure on LogicInt and is invoked directly in RationalsFromLogic.add_mul' and ratRel_trans. It also supports Gap45.Derivation.lcm_360_forces_D_eq_3, which forces D = 3 from the eight-tick octave. The module summary records that full ring axioms and the ring isomorphism LogicInt ≃+* Int remain open for follow-up.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.