English
If two expressions a and b are equivalent in PreEnvelGroupRel', then their images under mapAux f are equal.
Русский
Если выражения a и b эквивалентны в PreEnvelGroupRel', то их образы mapAux f равны.
LaTeX
$$$\forall a,b:\ PreEnvelGroupRel'\! R\ a\ b \Rightarrow toEnvelGroup.mapAux\ f\ a = toEnvelGroup.mapAux\ f\ b.$$$
Lean4
/-- Show that `toEnvelGroup.mapAux` sends equivalent expressions to equal terms.
-/
theorem well_def {R : Type*} [Rack R] {G : Type*} [Group G] (f : R →◃ Quandle.Conj G) :
∀ {a b : PreEnvelGroup R}, PreEnvelGroupRel' R a b → toEnvelGroup.mapAux f a = toEnvelGroup.mapAux f b
| _, _, PreEnvelGroupRel'.refl => rfl
| _, _, PreEnvelGroupRel'.symm h => (well_def f h).symm
| _, _, PreEnvelGroupRel'.trans hac hcb => Eq.trans (well_def f hac) (well_def f hcb)
| _, _, PreEnvelGroupRel'.congr_mul ha hb => by simp [toEnvelGroup.mapAux, well_def f ha, well_def f hb]
| _, _, congr_inv ha => by simp [toEnvelGroup.mapAux, well_def f ha]
| _, _, assoc a b c => by apply mul_assoc
| _, _, PreEnvelGroupRel'.one_mul a => by simp [toEnvelGroup.mapAux]
| _, _, PreEnvelGroupRel'.mul_one a => by simp [toEnvelGroup.mapAux]
| _, _, PreEnvelGroupRel'.inv_mul_cancel a => by simp [toEnvelGroup.mapAux]
| _, _, act_incl x y => by simp [toEnvelGroup.mapAux]
